File: r-and-i-answer-key-input.lsp

package info (click to toggle)
acl2 8.6%2Bdfsg-2
links: PTS
area: main
in suites: trixie
size: 1,111,420 kB
sloc: lisp: 17,818,294; java: 125,359; python: 28,122; javascript: 23,458; cpp: 18,851; ansic: 11,569; perl: 7,678; xml: 5,591; sh: 3,976; makefile: 3,833; ruby: 2,633; yacc: 1,126; ml: 763; awk: 295; csh: 233; lex: 197; php: 178; tcl: 49; asm: 23; haskell: 17
file content (4501 lines) | stat: -rw-r--r-- 125,118 bytes
parent folder | download | duplicates (2)
; Copyright (C) 2022, ForrestHunt, Inc.
; Written by J Strother Moore
; License: A 3-clause BSD license.  See the LICENSE file distributed with ACL2.
; Release approved by DARPA with "DISTRIBUTION STATEMENT A. Approved
; for public release. Distribution is unlimited."

; Recursion and Induction:  Answer Key
; J Strother Moore

; Updated October 2022 by Matt Kaufmann for latest R&I and to produce output
; that can be checked during ACL2 regression testing.

; NOTE: Readers of "Recursion and Induction" would be best served by looking
; not at the present file, but rather, at file:
; r-and-i-answer-key-log.txt

(in-package "ACL2")

; This file provides input for generating output file
; r-and-i-answer-key-log.out when certifying the book,
; r-and-i-answer-key-book.lisp.  In particular, that output file contains the
; comments below that are delimited by #{""" ... """}.  The certification
; process checks that r-and-i-answer-key-log.out agrees with the "golden"
; output file, r-and-i-answer-key-log.txt.

:----- #{"""

; This file was generated by ACL2 from the input file
; r-and-i-answer-key-input.lsp.  The output generated up to
; this point should be ignored by anyone who reads it.

; When the problem requires that you show a term or answer a
; question informally, the answer is written as a comment.

; We answer some ``fill in the blank'' questions by showing
; a theorem.  For example, if the question were to ask you
; to show the constant that is equal to (expt 2 31), we
; might show the theorem (equal (expt 2 31) 2147483648).

; We answer definition problems by just showing the
; appropriate defun.  Sometimes we have to provide the right
; measure.  For example,

; (defun f (x)
;  (declare (xargs :measure (ms x)))
;  <body>)

; means

;   The definition (defun f (x) <body>) is admissible under
;   the ACL2 definitional principle if you use the measure
;   (ms x) as the sense of the size of the argument.

; When the problem requires you to do a proof in the logic,
; we generally answer by showing an ACL2 command of the
; form

; (theorem <Problem-i>
;          <formula>
;          :hints (("Goal" :induct <term>
;                          :enable (<name1>
;                                   ...
;                                   <namek>)))
;          :rule-classes <classes>)

; (Notice that the double-quote character (") is escaped
; with a backslash (\), which is similarly escaped, in
; the output file.)

; You can read this as follows.

;   <Problem-i> is the challenge to prove the theorem
;   <formula>.

;   Proof: Induct as suggested by <term>, i.e., to unwind
;   the recursive function in the term <term>.  Then,
;   simplify each case.  The simplification may freely use
;   propositional calculus, axioms, definitions, and lemmas
;   about arithmetic.  However, the proof will require you
;   to use certain lemmas proved earlier in this file,
;   namely those whose names, <name1>, ..., <namek>, are
;   listed.  Q.E.D.

;   If no :induct <term> is given, induction is not necessary
;   to the proof; simplification alone sufficies.

;   If no names are listed, then propositional calculus,
;   axioms, definitions, and arithmetic suffice.

;   If no hints at all are given, it is as though no :induct
;   <term> is given and no lemmas are named, i.e., the proof
;   is by straightforward simplification.

;   You can ignore the :rule-classes entry <classes>; it
;   just tells the mechanical theorem prover how to use this
;   theorem in the future.

;   If you want to see the actual proof output produced by
;   ACL2 when carrying out this high-level description of
;   the proof, inspect the file r-and-i-answer-key-log.txt.

;   In the script below, the first time we use an :induct
;   hint we include as a comment the output you'll find in
;   r-and-i-answer-key-log.txt so you can see how the output
;   elaborates the proof sketch provided by the input.
;   Similarly, we provide output the first time we use an
;   :in-theory hint to list the names of relevant lemmas.

; There is no need for you to understand how we define the
; theorem command to make this happen.  So skip the
; following defmacro and go to the solution of Problem 1.

; WARNING: If you start using ACL2 we do not recommend that
; you use the theorem macro.  Instead, use defthm directly.
; Theorem has the same interface as defthm but (a) no
; induction is done automatically -- you have to give the
; induction hint explicitly and no proof has more than one
; induction, and (b) after the new theorem is proved and
; installed as a rule, the new rule is disabled.  The latter
; feature then forces us to enable each rule proved with
; theorem whenever we want to use it.  Together features (a)
; and (b) ensure that a theorem command pretty much has all
; the information you need to reconstruct the proof
; yourself.  It is far better to get used to the idea that
; ACL2 often chooses the right induction(s) and uses rules
; freely after you've proved them.  So use defthm instead of
; reproducing this macro in your scripts.
"""}

(defmacro theorem
  (name form
        &key (rule-classes ':rewrite rule-classes-suppliedp)
        hints)
  (let ((old-hints hints)
        (hints
         (cond ((null hints)
                '(("Goal" :do-not-induct t
                          :do-not '(generalize))))
               ((and (true-listp hints)
                     (equal (length hints) 1)
                     (equal (car (car hints)) "Goal"))
                `(("Goal"
                   :do-not-induct t
                   :do-not '(generalize)
                   ,@(cdr (car hints)))))
               (t nil))))

; Note that if hints is nil, something bad has happened and
; we detect it and react below.
                      
    (cond
     ((null hints)
      `(er soft 'theorem
           "The :hints value ~x0 is not allowed ~
            by this macro."
           ',old-hints))
     ((and rule-classes-suppliedp
           (equal rule-classes nil))
      `(defthm ,name ,form
         :rule-classes nil
         :hints ,hints))
     (t `(progn
           (defthm ,name ,form
             ,@(if rule-classes-suppliedp
                   `(:rule-classes ,rule-classes)
                 nil)
             :hints ,hints)
           (in-theory (disable ,name))
           (value-triple ',name))))))

(set-gag-mode nil)
(set-state-ok t)

:next-problem #{"""
; ------------------------------------------------------------
; Problem 1.
; 1. Monday                      symbol
; 2. greek letter pi             ill-formed (not ASCII)
; 3. HelloWorld!                 symbol 
; 4. --1                         symbol (!)
; 5. -1                          integer
; 6. *PI*                        symbol
; 7. 31415x10**-4                symbol
; 8. (A . B . C)                 ill-formed (illegal dot)
; 9. Hello World!                ill-formed (two symbols)
; 10. if                         symbol
; 11. invokevirtual              symbol
; 12. ((1) . (2))                pair
; 13. <=                         symbol
; 14. ((A . 1) (B . 2) (C . 3))  pair
; 15. Hello_World!               symbol
; 16. +                          symbol
; 17. lo-part                    symbol
; 18. 31415926535897932384626433832795028841971693993751058209749445923
;                                integer 
; 19. (1 . (2 . 3))              pair
; 20. (1 . 2 3)                  ill-formed (illegal dot)
; 21. "Hello World!"             string
; 22. ((1) (2) . 3)              pair
; 23. ()                         symbol (nil)
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 2.

; Rather than just show the answer, I'll define a function to do it
; and then show the result.

; I freely use full ACL2 here since this function isn't part of the
; answer!

; The theorem below equates our computation of the equivalence
; classes with an object that associates each value with the labels
; of all expressions that represent it.  Here is that list.

;            constant          labels
;         '(((1 2 3)           (1 11))
;           ((NIL NIL NIL)     (2))
;           (((NIL NIL))       (3))
;           ((1 (2 . 3) 4)     (4 6))
;           ((NIL NIL)         (5 10 12))
;           ((HELLOWORLD !)    (7))
;           ((1 (2 3) 4)       (8))
;           (((A . T) (B) (C)) (9 16))
;           ((A B C)           (13 14))
;           ((HELLO WORLD !)   (15))))
"""}

(defun add-label-to-bucket (label const buckets)
  (if (endp buckets)
      (list (list const (list label)))
    (if (equal const (car (car buckets)))
        (cons (list const (append (cadr (car buckets)) (list label)))
              (cdr buckets))
      (cons (car buckets)
            (add-label-to-bucket label const (cdr buckets))))))

(defun make-equiv-classes (alist buckets)
  (if (endp alist)
      buckets
    (make-equiv-classes (cdr alist)
                        (add-label-to-bucket (caar alist)
                                             (cadr (car alist))
                                             buckets))))

; Implementation note (can be ignored by the reader):
; Because everything in a certified book has to be a theorem, I
; state the answer as the equivalence of the question and the answer:

(theorem problem-2
  (equal (make-equiv-classes 

; Implementation note (can be ignored by the reader; this is already
; explained above):
; Here is an alist representing the question, a bunch of labeled
; constants.

          '((1 (1 . (2 3)))
            (2 (nil . (nil nil)))
            (3 ((nil nil) . nil))
            (4 (1 (2 . 3) 4))
            (5 (nil nil))
            (6 (1 (2 . 3) . (4 . ())))
            (7 (HelloWorld !))
            (8 (1 (2 3 . ()) 4))
            (9 ((A . t) (B . nil)(C . nil)))
            (10 (()()))
            (11 (1 2 3))
            (12 (() () . nil))
            (13 (A B C))
            (14 (a . (b . (c))))
            (15 (HELLO WORLD !))
            (16 ((a . t) (b) . ((c)))))
          nil)

; Here is the answer, showing the labels of equivalent constants.

;           constant          labels
         '(((1 2 3)           (1 11))
           ((NIL NIL NIL)     (2))
           (((NIL NIL))       (3))
           ((1 (2 . 3) 4)     (4 6))
           ((NIL NIL)         (5 10 12))
           ((HELLOWORLD !)    (7))
           ((1 (2 3) 4)       (8))
           (((A . T) (B) (C)) (9 16))
           ((A B C)           (13 14))
           ((HELLO WORLD !)   (15))))
  :rule-classes nil)

:next-problem #{"""
; ------------------------------------------------------------
; Problem 3.

; 1. (car (cdr x))                yes
; 2. (cons (car x y) z)           no - car takes 1 arg
; 3. (cons 1 2)                   no - constants must be quoted
; 4. (cons '1 '2)                 yes
; 5. (cons one two)               yes - one and two are variable symbols
; 6. (cons 'one 'two)             yes - 'one and 'two are constants
; 7. (equal '1 (car (cons '2 '3)))yes
; 8. (if t 1 2)                   no - constants must be quoted
; 9. (if 't '1 '2)                yes
; 10. (car (cons (cdr hi-part) (car lo-part)))    yes
; 11. car(cons x y)               no - wrong syntax
; 12. car(cons(x,y))              no - wrong syntax
; 13. (cons 1 (2 3 4))            no - constants must be quoted
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 4.
"""}

(theorem problem-4
  (and (equal '((1 . 2) . (3 . 4))            ; 1.
              (cons (cons '1 '2)
                    (cons '3 '4)))
       (equal '(1 2 3)                        ; 2.
              (cons '1
                    (cons '2
                          (cons '3 'nil))))
       (equal '((1 . t) (2 . nil) (3 . t))    ; 3.
              (cons (cons '1 't)
                    (cons (cons '2 'nil)
                          (cons (cons '3 't)
                                'nil))))
       (equal '((A . 1) (B . 2))              ; 4.
              (cons (cons 'a '1)
                    (cons (cons 'b '2)
                          'nil))))
  :rule-classes nil)

:next-problem #{"""
; ------------------------------------------------------------
; Problem 5.
"""}

(theorem problem-5
  (and (equal (cons (cons '1 '2) (cons (cons '3 '4) 'nil))  ; 1. 
              '((1 . 2) (3 . 4)))
       (equal (cons '1 (cons '2 '3))                        ; 2.
              '(1 2 . 3))
       (equal (cons 'nil (cons (cons 'nil 'nil) 'nil))      ; 3.
              '(nil (nil)))
       (equal (if 'nil '1 '2)                               ; 4.
              '2)
       (equal (if '1 '2 '3)                                 ; 5.
              '2)
       (equal (equal 'nil (cons 'nil 'nil))                 ; 6.
              'nil)
       (equal (equal 'Hello 'HELLO)                         ; 7.
              't)
       (equal (equal (cons '1 '2) (cons '1 'two))           ; 8.
              'nil))
  :rule-classes nil)

:next-problem #{"""
; ------------------------------------------------------------
; Problem 6.

; Answer: (car (cons (car a) (cons (cdr x) (cons '"Hello" z))))
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 7.

; 1. (cons '1 (cons '2 (cons '3 'nil)))
; 2. (equal '"Hello" hello)
; 3. (and (or a1 (or a2 a3))
;         (and (or b1 (or b2 b3))
;              (or c1 (or c2 c3))))
; 4. (equal x (cons 'or (cons 'a1 (cons 'a2 (cons 'a3 'nil)))))
; 5. (cons cons
;          (cons 'cons
;                (cons 'cons
;                      (cons (cons 'quote (cons 'cons 'nil))
;                            'nil))))
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 8.
"""}

(defun app (x y)
  (if (consp x)
      (cons (car x) (app (cdr x) y))
    y))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 9.
"""}

(defun rev (x)
  (if (consp x)
      (app (rev (cdr x)) (cons (car x) nil))
    nil))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 10.
"""}

(defun mapnil (x)
  (if (consp x)
      (cons nil (mapnil (cdr x)))
    nil))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 11.
"""}

(defun swap-tree (x)
  (if (consp x)
      (cons (swap-tree (cdr x))
            (swap-tree (car x)))
    x))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 12.
"""}

(defun mem (e x)
  (if (consp x)
      (if (equal e (car x))
          t
        (mem e (cdr x)))
    nil))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 13.
"""}

(defun sub (x y)
  (if (consp x)
      (if (mem (car x) y)
          (sub (cdr x) y)
        nil)
    t))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 14.
"""}

(defun int (x y)
  (if (consp x)
      (if (mem (car x) y)
          (cons (car x) (int (cdr x) y))
        (int (cdr x) y))
    nil))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 15.
"""}

(defun tip (e x)
  (if (consp x)
      (or (tip e (car x))
          (tip e (cdr x)))
    (equal e x)))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 16.
"""}

(defun flatten (x)
  (if (consp x)
      (app (flatten (car x))
           (flatten (cdr x)))
    (cons x nil)))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 17.
"""}

(defun evenlen (x)
  (if (consp x)
      (if (consp (cdr x))
          (evenlen (cdr (cdr x)))
        nil)
    t))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 18.

; Theorem. (and p q) /= nil  <-> p /= nil & q /= nil.

; Proof. We consider three cases.  We use lhs and rhs to refer to the
; left and right sides of the equivalence operator.  Because of the
; way we break the cases, it is straightforward to determine the value
; of the rhs and we write it in parentheses at the top of each case.
; We show the lhs has the same truthvalue.

; Case 1.  p /= nil & q /= nil  (rhs is true)
; (and p q) = q /= nil.  Thus lhs is true.

; Case 2.  p /= nil & q  = nil  (rhs is false)
; (and p q) = q = nil.  Thus lhs is false.

; Case 3.  p  = nil             (rhs is false)
; (and p q) = nil.  Thus lhs is false.

; Q.E.D.
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 19.

; Theorem. (or p q) /= nil <-> p /= nil v q /= nil.

; Proof. We consider three cases and use the same format as the proof
; in Problem 18.

; Case 1. p /= nil  (rhs is true)
; (or p q) = p /= nil.  Thus lhs is true.

; Case 2. p  = nil and q /= nil  (rhs is true)
; (or p q) = q /= nil.  Thus lhs is true.

; Case 3. p  = nil & q  = nil  (rhs is false)
; (or p q) = nil.  Thus lhs is false.

; Q.E.D.
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 20.

; Theorem. (implies p q) /= nil <-> (p /= nil -> q /= nil).

; Proof.  Same format as 18.

; Case 1. p /= nil and q /= nil (rhs is true)
; (implies p q) = t.  Thus lhs is true.

; Case 2. p /= nil and q  = nil (rhs is false)
; (implies p q) = nil.  Thus lhs is false.

; Case 3. p  = nil              (rhs is true)
; (implies p q) = t.  Thus lhs is true.

; Q.E.D.
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 21.

; Theorem. (iff p q) /=  <-> (p /= nil <-> q /= nil)

; Proof. We consider four cases.

; Case 1.  p /= nil and q /= nil (rhs is true)
; (iff p q)
;  = (and (implies p q) (implies q p))
;  = (and t t)
;  = t.
; Thus lhs is true.

; Case 2.  p /= nil and q  = nil (rhs is false)
; (iff p q)
;  = (and (implies p q) (implies q p)) 
;  = (and nil t)
;  = nil.
; Thus lhs is false.

; Case 3.  p  = nil and q /= nil (rhs is false)
; (iff p q)
;  = (and (implies p q) (implies q p)) 
;  = (and t nil)
;  = nil.
; Thus lhs is false.

; Case 4.  p  = nil and q  = nil (rhs is true)
; (iff p q)
;  = (and (implies p q) (implies q p)) 
;  = (and t t)
;  = t.
; Thus lhs is true.

; Q.E.D.
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 22.

; Theorem.  (equal x y) /= nil  <->  (x = y)

; Proof.

; Case 1.  x=y (rhs is true)
; (equal x y) = t, by Axiom 5.  Thus lhs is true.

; Case 2.  x /= y (rhs is false)
; (equal x y) /= t, by Axiom 5.  Thus, by Axiom 4,
; (equal x y) = nil.  Thus, lhs is false.

; Q.E.D.
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 23.

; Theorem.  (implies (and p (implies q r)) s) <->
;           ((p & -q) -> s) & ((p & q & r) -> s)

; Proof.  The proof will also establish the intermediate formula
; requested.  

; Since the lhs above is a term treated as a formula, the lhs is

; (implies (and p (implies q r)) s) /= nil

; <->

; (and p (implies q r)) /= nil -> (s /= nil)

; <->

; ((p /= nil) & (implies q r) /= nil) -> (s /= nil)

; <->

; (p /= nil) & (q /= nil -> r /= nil) -> (s /= nil)

; <->

; (p & (q -> r)) -> s

; We won't use this last formula, since it uses terms as formulas.
; Instead, we'll go back one step:

; (p /= nil) & (q /= nil -> r /= nil) -> (s /= nil)

; <->

; (q  = nil) -> ((p /= nil) & (q /= nil -> r /= nil) -> (s /= nil))
; &
; (q /= nil) -> ((p /= nil) & (q /= nil -> r /= nil) -> (s /= nil))

; The previous step is just the tautology a <-> ((-b -> a) & (b -> a)).
; Continuing, using (a -> (b -> c)) <-> ((a & b) -> c)

; <->

; (q  = nil) & (p /= nil) & (q /= nil -> r /= nil) -> (s /= nil)
; &
; (q /= nil) * (p /= nil) & (q /= nil -> r /= nil) -> (s /= nil)

; <->

; (p /= nil) & (q  = nil) & t -> (s /= nil)
; &
; (p /= nil) & (q /= nil) & (r /= nil) -> (s /= nil)

; <->

; (p & -q) -> s
; &
; (p & q & r) -> s

; Q.E.D.

; This proof was tedious only because we tried to show some of the
; propositional calculus steps.
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 24.

; Theorem.  (equal (car (if a b c)) (if a (car b) (car c)))

; Proof.  We will reduce the lhs, (car (if a b c)), to the rhs, (if a
; (car b) (car c)), under two cases, thus establishing lhs=rhs and
; thus (equal lhs rhs).

; Case 1.  a /= nil.

; lhs = (car (if a b c)) = (car b)
; rhs = (if a (car b) (car c)) = (car b).

; Case 2.  a  = nil.

; lhs = (car (if a b c)) = (car c)
; rhs = (if a (car b) (car c)) = (car c).

; Q.E.D.
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 25.

; Theorem.  (equal (if (if a b c) x y)
;                  (if a (if b x y) (if c x y)))

; Proof.  Cases on a.  We take even bigger steps than in Problem 24.

; Case 1. a /= nil.
; lhs = (if b x y) = rhs.

; Case 2. a  = nil.
; lhs = (if c x y) = rhs.

; Q.E.D.
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 26.

; Theorem.  (equal (treecopy (cons a b))
;                  (cons (treecopy a) (treecopy b)))

; Proof.  
; (treecopy (cons a b))
; =                                          {by def treecopy}
; (if (consp (cons a b))
;     (cons (treecopy (car (cons a b)))
;           (treecopy (cdr (cons a b))))
;     (cons a b))
; =                                          {by Axiom 7}
; (if t
;     (cons (treecopy (car (cons a b)))
;           (treecopy (cdr (cons a b))))
;     (cons a b))
; =                                          {by Axiom 1 and 2}
; (cons (treecopy (car (cons a b)))
;       (treecopy (cdr (cons a b))))
; =                                          {by Axiom 9 and 10}
; (cons (treecopy a)
;       (treecopy b))
; Q.E.D.
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 27.

; Proof that 'June = 'July (under the scenario described).

; While f is defined as initially shown, prove the theorem
; Lemma 1:  (f x) = 1.
; After the redefinition, prove the theorem
; Lemma 2:  (f x) = 2.
; By transitivity of equality and Lemmas 1 and 2, 1 = 2.  By
; propositional calculus, we know that if p is a theorem, then 
; -p -> q.  Hence,

; (1 /= 2) -> 'June = 'July.

; By Axiom 1, we know (1 /= 2).  Thus

; 'June = 'July

; Q.E.D.

; Of course, the crux of this proof is establishing any contradiction.
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 28.

; Proof that 1=2, given (defun f (x) (cons x y)).

; Lemma 1: (cdr (f x)) = y.  Proof: by def f and Axiom 10.  Q.E.D.

; Thus, 
; (cdr (f 0)) = 1             {instantiation of Lemma 1}
; (cdr (f 0)) = 2             {instantiation of Lemma 1}
; 1=2                         {trans of equality}
; Q.E.D.
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 29.

; Proof that t=nil, given (defun f (x) (not (f x))).

; First observe that (f x) = (if (f x) nil t).  Thus,
; since (f x) = nil or (f x) /= nil, we know that (f x)
; is either t or nil.  Consider the two cases.

; Case 1.  (f x) = t
; (f x) = (not (f x)) = (not t) = nil.

; Case 2.  (f x) = nil
; (f x) = (not (f x)) = (not nil) = t.

; Q.E.D.
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 30.

; Restriction 1 prevents the redefinition of a function, as 
; tried in Problem 27.  Restriction 3 prevents the use of
; global variables, as tried in Problem 28.  Restriction 4
; prevents the silly recursion, as tried in Problem 29.
; In particular, x is not a car/cdr nest and so the definition
; of f in Problem 29 is not acceptable.
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 31.

; Yes, because (consp x) governs a recursive call on a
; car/cdr nest around x, namely the nest (cdr (cdr x)).
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 32.

; No.  The only governing test is (consp x) but the only car/cdr nest
; in recursion is around y.
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 33.

; No.  The governing test, (consp x), is for the first formal but the
; first actual in the recursive call is not a car/cdr nest around the
; first formal.  This is how the answer to Problem 32 should read!
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 34.

; Yes, because (consp x) governs the recursive call (f (cdr (cdr x))),
; and (cdr (cdr x)) is a car/cdr nest around x.
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 35.

; No, because (consp x) does not govern the recursive call.  There is
; no (consp x) anywhere in the definition.  (not (endp x)) governs the
; recursive call and that is not syntactically identical to (consp x).
; However, it is logically equivalent and we will eventually improve
; the definitional principle so that definitions like this are
; allowed.
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 36.

; Yes.  (Consp x) governs a recursion on a car/cdr nest around x in
; the same argument position.  It doesn't matter what happens in other
; argument positions.
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 37.

; Yes, for the same reasons given in Problem 36.
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 38.

; No.  If the first defun is allowed, then we have an axiom about g
; and then we cannot ``redefine'' g with the second defun.  The
; symmetric argument blocks defining them in the other order.
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 39.

; No.  All we can do is expand the definition of (f x) and
; consider cases.  We can construct a ``proof'' like this:

; Case 1:  (not (consp x))
; (f x) = t {by def f} 

; Case 2:  (consp x) & (not (consp (cdr x)))
; (f x) = (f (cdr x)) = t {by def f}

; Case 3:  (consp x) & (consp (cdr x)) & (not (consp (cdr (cdr x))))
; (f x) = (f (cdr x)) = (f (cdr (cdr x))) = t {by def f}

; ...

; But we cannot reach the terminal case of the recursion unless we
; know how long x is.  And infinite proofs are not allowed!
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 40.
"""}

(theorem problem-40
         (equal (app (app a b) c)
                (app a (app b c)))

         :hints (("Goal"
                  :induct (app a b))))

:----- #{"""
; Here is the proof output you'll find for this event in
; r-and-i-answer-key-log.txt.  Notice that the output prints the
; induction scheme suggested by the hint.

[Note:  A hint was supplied for the goal above.  Thanks!]

Name the formula above *1.

We have been told to use induction.  One induction scheme is suggested
by the induction hint.  

We will induct according to a scheme suggested by (APP A B).  This
suggestion was produced using the :induction rule APP.  If we let (:P A B C)
denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP A)) (:P A B C))
     (IMPLIES (AND (CONSP A) (:P (CDR A) B C))
              (:P A B C))).
This induction is justified by the same argument used to admit APP.
When applied to the goal at hand the above induction scheme produces
two nontautological subgoals.

Subgoal *1/2
(IMPLIES (NOT (CONSP A))
         (EQUAL (APP (APP A B) C)
                (APP A (APP B C)))).

But simplification reduces this to T, using the :definition APP and
primitive type reasoning.

Subgoal *1/1
(IMPLIES (AND (CONSP A)
              (EQUAL (APP (APP (CDR A) B) C)
                     (APP (CDR A) (APP B C))))
         (EQUAL (APP (APP A B) C)
                (APP A (APP B C)))).

But simplification reduces this to T, using the :definition APP, primitive
type reasoning and the :rewrite rules CAR-CONS and CDR-CONS.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM PROBLEM-40 ...)
Rules: ((:DEFINITION APP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION APP)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS))
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 41.
"""}

(theorem problem-41-counterexample
  (not (equal (app '(1 2 3 . 4) nil)
              '(1 2 3 . 4)))
  :rule-classes nil)

(defun proper (x)
  (if (consp x)
      (proper (cdr x))
    (equal x nil)))

(theorem problem-41
         (implies (proper x)
                  (equal (app x nil) x))

         :hints (("Goal"
                  :induct (app x nil))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 42.
"""}

(theorem problem-42
         (equal (mapnil (app a b))
                (app (mapnil a) (mapnil b)))

         :hints (("Goal"
                  :induct (app a b))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 43.
"""}

(theorem problem-43
         (equal (rev (mapnil x))
                (mapnil (rev x)))

         :hints (("Goal"
                  :induct (rev x)
                  :in-theory (enable problem-42))))

:----- #{"""
; Here is the output generated.  You can find similar output
; for every theorem in r-and-i-answer-key-log.txt.  Note that
; the output makes it clear which subgoal requires Problem-42.
; In addition, the output lists all the rules used.  All of
; the rules below, except Problem-42, are part of the basic
; propositional calculus, axioms, definitions, and
; arithmetic we allow ourselves to use freely in Recursion
; and Induction.

[Note:  A hint was supplied for the goal above.  Thanks!]

Name the formula above *1.

We have been told to use induction.  One induction scheme is suggested
by the induction hint.  

We will induct according to a scheme suggested by (REV X).  This suggestion
was produced using the :induction rule REV.  If we let (:P X) denote
*1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP X)) (:P X))
     (IMPLIES (AND (CONSP X) (:P (CDR X)))
              (:P X))).
This induction is justified by the same argument used to admit REV.
When applied to the goal at hand the above induction scheme produces
two nontautological subgoals.

Subgoal *1/2
(IMPLIES (NOT (CONSP X))
         (EQUAL (REV (MAPNIL X))
                (MAPNIL (REV X)))).

But simplification reduces this to T, using the :definitions MAPNIL
and REV and the :executable-counterparts of EQUAL, MAPNIL and REV.

Subgoal *1/1
(IMPLIES (AND (CONSP X)
              (EQUAL (REV (MAPNIL (CDR X)))
                     (MAPNIL (REV (CDR X)))))
         (EQUAL (REV (MAPNIL X))
                (MAPNIL (REV X)))).

But simplification reduces this to T, using the :definitions MAPNIL
and REV, the :executable-counterparts of CONS and MAPNIL, primitive
type reasoning, the :rewrite rules CAR-CONS, CDR-CONS and PROBLEM-42
and the :type-prescription rule MAPNIL.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM PROBLEM-43 ...)
Rules: ((:DEFINITION MAPNIL)
        (:DEFINITION REV)
        (:EXECUTABLE-COUNTERPART CONS)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART MAPNIL)
        (:EXECUTABLE-COUNTERPART REV)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION REV)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE PROBLEM-42)
        (:TYPE-PRESCRIPTION MAPNIL))
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 44.
"""}

(theorem problem-44-counterexample
  (not (equal (rev (rev '(1 2 3 . 4)))
              '(1 2 3 . 4)))
  :rule-classes nil)

(theorem problem-44c
         (equal (proper (app a b))
                (proper b))

         :hints (("Goal"
                  :induct (app a b))))

(theorem problem-44b
         (proper (rev x))

         :hints (("Goal"
                  :induct (rev x)
                  :in-theory (enable problem-44c))))

(theorem problem-44a
         (equal (rev (app a b))
                (app (rev b) (rev a)))

         :hints (("Goal"
                  :induct (app a b)
                  :in-theory (enable problem-40
                                     problem-41
                                     problem-44b))))

(theorem problem-44
         (implies (proper x)
                  (equal (rev (rev x)) x))

         :hints (("Goal"
                  :induct (rev x)
                  :in-theory (enable problem-44a))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 45.
"""}

(theorem problem-45
         (equal (swap-tree (swap-tree x)) x)

         :hints (("Goal"
                  :induct (swap-tree x))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 46.
"""}

(theorem problem-46
         (equal (mem e (app a b))
                (or (mem e a)
                    (mem e b)))

         :hints (("Goal"
                  :induct (mem e a))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 47.
"""}

(theorem problem-47a
         (implies (not (mem e b))
                  (not (mem e (int a b))))

         :hints (("Goal"
                  :induct (int a b))))

(theorem problem-47
         (equal (mem e (int a b))
                (and (mem e a)
                     (mem e b)))

         :hints (("Goal"
                  :induct (mem e a)
                  :in-theory (enable problem-47a))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 48.
"""}

(theorem problem-48a
         (implies (sub x (cdr y))
                  (sub x y))

         :hints (("Goal"
                  :induct (sub x y))))

(theorem problem-48
         (sub x x)

         :hints (("Goal"
                  :induct (sub x x)
                  :in-theory (enable problem-48a))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 49.
"""}

(theorem problem-49a
         (implies (and (mem e a)
                       (sub a b))
                  (mem e b))

         :hints (("Goal"
                  :induct (sub a b))))

(theorem problem-49
         (implies (and (sub a b)
                       (sub b c))
                  (sub a c))

         :hints (("Goal"
                  :induct (sub a c)
                  :in-theory (enable problem-48a
                                     problem-49a))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 50.
"""}

(theorem problem-50a
         (equal (sub (app a b) c)
                (and (sub a c)
                     (sub b c)))

         :hints (("Goal"
                  :induct (sub a c)
                  :in-theory (enable problem-48a
                                     problem-48
                                     problem-49a))))

(theorem problem-50
         (sub (app a a) a)

         :hints (("Goal"
                  :in-theory (enable problem-48
                                     problem-50a)))
         :rule-classes nil)

:next-problem #{"""
; ------------------------------------------------------------
; Problem 51.
"""}

(defun mapnil1 (x a)
  (if (consp x)
      (mapnil1 (cdr x) (cons nil a))
    a))

(defun nils (x)
  (if (consp x)
      (and (equal (car x) nil)
           (nils (cdr x)))
    (equal x nil)))

(theorem problem-51a
         (equal (mapnil1 a (cons nil b))
                (cons nil (mapnil1 a b)))

         :hints (("Goal"
                  :induct (mapnil1 a b))))

(theorem problem-51b
         (implies (nils x)
                  (equal (mapnil1 x nil) x))

         :hints (("Goal"
                  :induct (nils x)
                  :in-theory (enable problem-51a))))

(theorem problem-51
         (implies (and (nils a)
                       (nils b))
                  (equal (mapnil1 a b)
                         (mapnil1 b a)))

         :hints (("Goal"
                  :induct (mapnil1 a b)
                  :in-theory (enable problem-51a
                                     problem-51b))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 52.
"""}

(defun rm (x y)
  (if (consp y)
      (if (equal x (car y))
	  (cdr y)
	(cons (car y) (rm x (cdr y))))
    y))

(defun perm (x y)
  (if (consp x)
      (and (mem (car x) y)
           (perm (cdr x) (rm (car x) y)))
      (not (consp y))))



:next-problem #{"""
; ------------------------------------------------------------
; Problem 53.
"""}

(theorem problem-53
         (perm x x)

         :hints (("Goal"
                  :induct (perm x x))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 54.
"""}

(theorem problem-54a
         (implies (mem a x)
                  (equal (perm x (cons a y))
                         (perm (rm a x) y)))

         :hints (("Goal"
                  :induct (perm x y))))

(theorem problem-54
         (implies (perm x y)
                  (perm y x))

         :hints (("Goal"
                  :induct (perm x y)
                  :in-theory (enable problem-54a))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 55.
"""}

(theorem problem-55a
         (implies (mem a (rm b x))
                  (mem a x))

         :hints (("Goal"
                  :induct (mem a x))))

(theorem problem-55b
         (implies (and (perm x y)
                       (mem a x))
                  (mem a y))

         :hints (("Goal"
                  :induct (perm x y)
                  :in-theory (enable problem-55a))))

(theorem problem-55c
         (equal (rm a (rm b x))
                (rm b (rm a x)))

         :hints (("Goal"
                  :induct (rm a x))))

(theorem problem-55d
         (implies (and (not (equal e d))
                       (mem e x))
                  (mem e (rm d x)))

         :hints (("Goal"
                  :induct (rm d x)
                  :in-theory (enable problem-48
                                     problem-49a))))

(theorem problem-55e
         (implies (perm x y)
                  (perm (rm a x)
                        (rm a y)))

         :hints (("Goal"
                  :induct (perm x y)
                  :in-theory (enable problem-54a
                                     problem-54
                                     problem-55c
                                     problem-55d))))

(theorem problem-55
         (implies (and (perm x y)
                       (perm y z))
                  (perm x z))

         :hints (("Goal"
                  :induct (list (perm x y) (perm x z))
                  :in-theory (enable problem-54
                                     problem-55b
                                     problem-55e))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 56.

; Before Problem 56, the document introduces a total order.  As
; explained in the document, <<= is intended as a more suggestive name
; than the ACL2 built-in relation lexorder.
"""}

(defun <<= (x y) (lexorder x y))

:----- #{"""
; ACL2 has already proved that lexorder is a non-strict total order.
; So this lemma about <<= is trival and unnecessary.
"""}

(theorem <<=-non-strict-total-order
  (and (<<= x x)
       (implies (and (<<= x y)
                     (<<= y x))  
                (equal x y))
       (implies (and (<<= x y)
                     (<<= y z))
                (<<= x z))
       (or (<<= x y)
           (<<= y x)))
  :rule-classes nil)

:----- #{"""
; Here is the solution to Problem 56.
"""}

(defun ordered (x)
  (if (consp x)
      (if (consp (cdr x))
          (and (<<= (car x) (cadr x))
               (ordered (cdr x)))
        t)
    t))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 57.
"""}

(defun insert (e x)
  (if (consp x)
      (if (<<= e (car x))
          (cons e x)
        (cons (car x)
              (insert e (cdr x))))
    (cons e nil)))

(defun isort (x)
  (if (consp x)
      (insert (car x)
              (isort (cdr x)))
    nil))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 58.
"""}

(theorem problem-58a
         (implies (ordered x)
                  (ordered (insert e x)))

         :hints (("Goal"
                  :induct (insert e x))))

(theorem problem-58
         (ordered (isort x))

         :hints (("Goal"
                  :induct (isort x)
                  :in-theory (enable problem-58a))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 59.

; I will show two proofs of Problem 59.
"""}

(theorem problem-59a
         (implies (perm a b)
                  (perm (insert e a) (cons e b)))

         :hints (("Goal"
                  :induct (perm a b)
                  :in-theory (enable problem-48
                                     problem-49a
                                     problem-54a
                                     problem-54))))

(theorem problem-59
         (perm (isort x) x)

         :hints (("Goal"
                  :induct (isort x)
                  :in-theory (enable problem-54
                                     problem-59a))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 60.
"""}

(theorem problem-60a
         (equal (insert e (insert d x))
                (insert d (insert e x)))

         :hints (("Goal"
                  :induct (insert e x))))
  
(theorem problem-60b
         (equal (isort (app x (list e)))
                (insert e (isort x)))

         :hints (("Goal"
                  :induct (isort x)
                  :in-theory (enable problem-60a))))

(theorem problem-60c
         (equal (isort (rev x))
                (isort x))

         :hints (("Goal"
                  :induct (isort x)
                  :in-theory (enable problem-60b))))

(theorem problem-60d
         (equal (isort (insert e x))
                (insert e (isort x)))

         :hints (("Goal"
                  :induct (insert e x)
                  :in-theory (enable problem-60a))))

(theorem problem-60e
         (equal (isort (isort x))
                (isort x))

         :hints (("Goal"
                  :induct (isort x)
                  :in-theory (enable problem-60d))))

(theorem problem-60
         (equal (isort (rev (isort l)))
                (isort l))

         :hints (("Goal"
                  
                  :in-theory (enable problem-60c
                                     problem-60e))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 61.
"""}

(defun rev1 (x a)
  (if (consp x)
      (rev1 (cdr x) (cons (car x) a))
    a))

(theorem problem-61a
         (equal (rev1 x a) (app (rev x) a))

         :hints (("Goal"
                  :induct (rev1 x a)
                  :in-theory (enable problem-40))))

(theorem problem-61
         (equal (rev1 x nil) (rev x))

         :hints (("Goal"
                  :in-theory (enable problem-41
                                     problem-44b
                                     problem-61a))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 62.

; This proof relies on the neat fact that we proved above
; (mapnil1 a (cons nil b)) = (cons nil (mapnil1 a b)).
"""}

(theorem problem-62-direct
         (equal (mapnil1 a nil)
                (mapnil a))

         :hints (("Goal"
                  :induct (mapnil a)
                  :in-theory (enable problem-51a))))

:----- #{"""
; Generally, a better way to prove theorems like this is to
; generalize the accumulator.  Here is that proof.
  
; Note that the following lemma is the analogue of the neat fact
; mentioned above.
"""}

(theorem problem-62a
         (implies (nils a)
                  (equal (app a (cons nil b))
                         (cons nil (app a b))))

         :hints (("Goal"
                  :induct (app a b))))

(theorem problem-62b
         (nils (mapnil a))

         :hints (("Goal"
                  :induct (mapnil a))))

(theorem problem-62c
         (equal (mapnil1 a b)
                (app (mapnil a) b))

         :hints (("Goal"
                  :induct (mapnil1 a b)
                  :in-theory (enable problem-62a
                                     problem-62b))))

(theorem problem-62d
         (proper (mapnil a))

         :hints (("Goal"
                  :induct (mapnil a))))

(theorem problem-62
         (equal (mapnil1 a nil)
                (mapnil a))

         :hints (("Goal"
                  :in-theory (enable problem-41
                                     problem-62c
                                     problem-62d))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 63.

; Theorem. x /= (cons x y)

; This fact is built into ACL2 so its proof is not enlightening.  But
; here a primitive proof and it is enlightening because it requires
; induction.

; Proof.  Induction on x.  

; Base Case:  
; (implies (not (consp x))
;          (not (equal x (cons x y))))
; Trivial, since the contrapositive is true by Axiom 7 and equality.

; Induction Step:
; (implies (and (consp x)
;               (not (equal (car x) (cons (car x) (cdr x)))))
;          (not (equal x (cons x y))))

; Note the unusual choice of induction hypothesis.  We replaced x
; by (car x) and y by (cdr x).
         
; So, given (consp x) and Axiom 11, the induction hypothesis becomes

;                (not (equal (car x) x))

; Now suppose the conclusion is false.  That is, suppose
; x = (cons x y).  Then take the car of both sides and we get
; (car x) = x.  Which is contradicted by the induction hypothesis.

; Q.E.D.
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 64.
"""}

(defun mcflatten (x a)
  (if (consp x)
      (mcflatten (car x)
                 (mcflatten (cdr x) a))
    (cons x a)))

(theorem problem-64a
         (equal (mcflatten x a)
                (app (flatten x) a))

         :hints (("Goal"
                  :induct (mcflatten x a)
                  :in-theory (enable problem-40))))

(theorem problem-64b
         (proper (flatten x))

         :hints (("Goal"
                  :induct (flatten x)
                  :in-theory (enable problem-44c))))

(theorem problem-64
         (equal (mcflatten x nil)
                (flatten x))

         :hints (("Goal"
                  :in-theory (enable problem-41
                                     problem-64a
                                     problem-64b))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 65.
"""}

(defun nat (x)
  (if (consp x)
      (and (equal (car x) nil)
           (nat (cdr x)))
    (equal x nil)))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 66.
"""}

(defun fix-nat (x)
  (if (consp x)
      (cons nil (fix-nat (cdr x)))
    nil))

:----- #{"""
; It is useful to know
"""}

(theorem problem-66a
         (nat (fix-nat x))

         :hints (("Goal"
                  :induct (fix-nat x))))

(theorem problem-66b
         (implies (nat x)
                  (equal (fix-nat x) x))

         :hints (("Goal"
                  :induct (nat x))))

(defun plus (x y)
  (if (consp x)
      (cons nil (plus (cdr x) y))
    (fix-nat y)))

(theorem problem-66c
         (nat (plus x y))

         :hints (("Goal"
                  :induct (plus x y)
                  :in-theory (enable problem-66a))))

(theorem problem-66d
         (equal (plus (fix-nat i) j)
                (plus i j))

         :hints (("Goal"
                  :induct (plus i j))))

(theorem problem-66e
         (equal (plus i (fix-nat j))
                (plus i j))

         :hints (("Goal"
                  :induct (plus i j)
                  :in-theory (enable problem-66a
                                     problem-66b))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 67.
"""}

(defun times (x y)
  (if (consp x)
      (plus y (times (cdr x) y))
    nil))

(theorem problem-67a
         (nat (times x y))

         :hints (("Goal"
                  :induct (times x y)
                  :in-theory (enable problem-66c))))

(theorem problem-67b
         (equal (times (fix-nat i) j)
                (times i j))

         :hints (("Goal"
                  :induct (times i j))))

(theorem problem-67c
         (equal (times i (fix-nat j))
                (times i j))

         :hints (("Goal"
                  :induct (times i j)
                  :in-theory (enable problem-66d))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 68.
"""}

(defun power (x y)
  (if (consp y)
      (times x (power x (cdr y)))
    '(nil)))

(theorem problem-68a
         (nat (power x y))

         :hints (("Goal"
                  :induct (power x y)
                  :in-theory (enable problem-67a))))

(theorem problem-68b
         (equal (power (fix-nat i) j)
                (power i j))

         :hints (("Goal"
                  :induct (power i j)
                  :in-theory (enable problem-67b))))

(theorem problem-68c
         (equal (power i (fix-nat j))
                (power i j))

         :hints (("Goal"
                  :induct (power i j))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 69.
"""}

(defun lesseqp (x y)
  (if (consp x)
      (if (consp y)
          (lesseqp (cdr x) (cdr y))
        nil)
    t))

(theorem problem-69a
         (equal (lesseqp (fix-nat i) j)
                (lesseqp i j))

         :hints (("Goal"
                  :induct (list (fix-nat i) (lesseqp i j)))))

:----- #{"""
; Note: I included (fix-nat i) in the :induct hint above because it
; forces the theorem prover to expand (fix-nat i) in the conclusion of
; the induction step.
"""}

(theorem problem-69b
         (equal (lesseqp i (fix-nat j))
                (lesseqp i j))

         :hints (("Goal"
                  :induct (lesseqp i j))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 70.
"""}

(defun evennat (x)
  (if (consp x)
      (if (consp (cdr x))
          (evennat (cdr (cdr x)))
        nil)
    t))

(theorem problem-70a
         (equal (evennat (fix-nat i))
                (evennat i))

         :hints (("Goal"
                  :induct (evennat i))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 71.

; We start with a general 0-identity for plus.
"""}

(theorem problem-71a
         (implies (not (consp z))
                  (equal (plus i z) (fix-nat i)))

         :hints (("Goal"
                  :induct (plus i z))))

(theorem problem-71
         (implies (nat i)
                  (equal (plus i nil) i))

         :hints (("Goal"
                  :in-theory (enable problem-66b
                                     problem-71a))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 72.
"""}

(theorem problem-72
         (equal (plus (plus i j) k)
                (plus i (plus j k)))

         :hints (("Goal"
                  :induct (plus i j)
                  :in-theory (enable problem-66b
                                     problem-66c
                                     problem-66d))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 73.
"""}

(theorem problem-73a
         (equal (plus i (cons x j))
                (cons nil (plus i j)))

         :hints (("Goal"
                  :induct (plus i j))))

(theorem problem-73
         (equal (plus i j)
                (plus j i))

         :hints (("Goal"
                  :induct (plus i j)
                  :in-theory (enable problem-71a
                                     problem-73a))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 74.

; Note that the following lemma is another sense of commutativity
; for plus.
"""}

(theorem problem-74a
         (equal (plus i (plus j k))
                (plus j (plus i k)))

         :hints (("Goal"
                  :induct (plus j k)
                  :in-theory (enable problem-66b
                                     problem-66c
                                     problem-66e
                                     problem-73a))))

(theorem problem-74b
         (equal (times (plus i j) k)
                (plus (times i k) (times j k)))

         :hints (("Goal"
                  :induct (times i k)
                  :in-theory (enable problem-66b
                                     problem-67a
                                     problem-67b
                                     problem-73
                                     problem-74a))))

(theorem problem-74
         (equal (times (times i j) k)
                (times i (times j k)))

         :hints (("Goal"
                  :induct (times i j)
                  :in-theory (enable problem-74b))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 75.
"""}

(theorem problem-75a
         (implies (not (consp z))
                  (equal (times i z) nil))

         :hints (("Goal"
                  :induct (times i z)
                  :in-theory (enable problem-71a
                                     problem-73))))

(theorem problem-75b
         (equal (times i (cons x j))
                (plus i (times i j)))

         :hints (("Goal"
                  :induct (times i j)
                  :in-theory (enable problem-71a
                                     problem-73
                                     problem-74a))))

(theorem problem-75
         (equal (times i j)
                (times j i))

         :hints (("Goal"
                  :induct (times i j)
                  :in-theory (enable problem-75a
                                     problem-75b))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 76.
"""}

(theorem problem-76a
         (equal (times i (plus j k))
                (plus (times i j)
                      (times i k)))

         :hints (("Goal"
                  :induct (times i k)
                  :in-theory (enable problem-72
                                     problem-73
                                     problem-74a))))

(theorem problem-76b
         (equal (times i (times j k))
                (times j (times i k)))

         :hints (("Goal"
                  :induct (times j k)
                  :in-theory (enable problem-75
                                     problem-76a))))

(theorem problem-76
         (equal (power b (plus i j))
                (times (power b i)
                       (power b j)))

         :hints (("Goal"
                  :induct (power b i)
                  :in-theory (enable problem-66b
                                     problem-68a
                                     problem-68c
                                     problem-73
                                     problem-75
                                     problem-76b))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 77.
"""}

(theorem problem-77a
         (equal (power (times a b) i)
                (times (power a i)
                       (power b i)))

         :hints (("Goal"
                  :induct (power b i)
                  :in-theory (enable problem-74
                                     problem-75
                                     problem-76b))))

(theorem problem-77b
         (equal (power '(nil) i)
                '(nil))

         :hints (("Goal"
                  :induct (power '(nil) i))))

(theorem problem-77
         (equal (power (power b i) j)
                (power b (times i j)))

         :hints (("Goal"
                  :induct (times i j)
                  :in-theory (enable problem-76
                                     problem-77a
                                     problem-77b))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 78.
"""}

(theorem problem-78
         (lesseqp i i)

         :hints (("Goal"
                  :induct (lesseqp i i))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 79.
"""}

(theorem problem-79
         (implies (and (lesseqp i j)
                       (lesseqp j k))
                  (lesseqp i k))

         :hints (("Goal"
                  :induct (list (lesseqp i j) (lesseqp i k)))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 80.
"""}

(theorem problem-80
         (equal (lesseqp (plus i j) (plus i k))
                (lesseqp j k))

         :hints (("Goal"
                  :induct (plus i k)
                  :in-theory (enable problem-69a
                                     problem-69b))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 81.
"""}

(theorem problem-81
         (implies (and (evennat i)
                       (evennat j))
                  (evennat (plus i j)))

         :hints (("Goal"
                  :induct (evennat i)
                  :in-theory (enable problem-70a
                                     problem-73
                                     problem-73a))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 82.
"""}

(defun cc (x)
  (if (consp x)
      (+ 1
         (+ (cc (car x))
            (cc (cdr x))))
    0))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 83.

; Theorem. (natp (cc x))

; Proof.  Induction on x.
; Base Case:  (not (consp x))
; (cc x) = 0.
; (natp 0) = t.

; Induction Step:
;  (implies (and (consp x)
;                (natp (cc (car x)))
;                (natp (cc (cdr x))))
;           (natp (cc x)))

; The conclusion becomes
; (natp (+ 1 (+ (cc (car x)) (cc (cdr x)))))
; and that follows by standard arithmetic from the induction
; hypotheses.

; Q.E.D.
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 84.

; (and (implies (consp x)
;               (< (cc (car x)) (cc x)))
;      (implies (consp x)
;               (< (cc (cdr x)) (cc x))))
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 85.
"""}

(theorem problem-85
  (and (implies (consp x)
                (< (cc (car x)) (cc x)))
       (implies (consp x)
                (< (cc (cdr x)) (cc x))))
  :rule-classes :linear)

:next-problem #{"""
; ------------------------------------------------------------
; Problem 86.

; Del was defined when we introduced perm.
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 87.
"""}

(theorem problem-87a
         (implies (mem e x)
                  (< (cc (rm e x)) (cc x)))

         :hints (("Goal"
                  :induct (cc x)))
         :rule-classes :linear)

(defun f23 (e x)
  (declare (xargs :measure (cc x)))
  (if (mem e x)
      (f23 e (rm e x))
    23))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 88.

; No.  We need to inductively assume that (f23 e (rm e x))
; is 23 to prove that (f e x) is 23.
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 89.

; Ack terminates because the second argument always either gets
; smaller or stays fixed.  But when the second argument stays fixed,
; the first argument gets smaller.
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 90.

; Rather than just show the answers, I write a function that computes
; the answers.  Again, I feel free to use any feature of ACL2, since
; this question did not require you to write these functions.

; By loading the file (certified book) below, we can write
; ordinals in a nice algebraic notation.  Thus, I can create my
; examples by writing expressions like:

;  (o+ (o* (o^ (omega) 3) 5)
;      (o* (o^ (omega) 1) 25)
;      7)

; instead of ((3 . 5) (1 . 25) . 7).
"""}

(include-book "ordinals/ordinals" :dir :system)

:----- #{"""
; So here is the function that checks a pair of ordinals and announces
; whether a<b, a=b, or a>b.
"""}

(defun check-row (row)
  (let ((a (car row))
        (b (cadr row)))
    (if (and (o-p a)
             (o-p b))
        (if (o< a b) 'a<b
            (if (equal a b) 'a=b 'b<a))
      'not-o-p!)))

:----- #{"""
; And now I check all the rows in a table.
; Here are the rows of that table with suitable column headers.

;                 a                      b                           answer
;           (1    23                     100                         A<B)
;           (2    1000000                ((1 . 1) . 0)               A<B)
;           (3    ((2 . 1) . 0)          ((1 . 2) . 0)               B<A)
;           (4    ((3 . 5) (1 . 25) . 7) ((3 . 5) (2 . 1) . 3)       A<B)
;           (5    ((((2 . 1) . 0) . 5) . 3)
;                                        ((((1 . 1) . 0) . 5) (1 . 25) . 7)
                                                                     B<A)))

"""}

(defun check-all-rows (tab i)
  (if (endp tab)
      nil
    (cons (list i (car (car tab)) (cadr (car tab)) (check-row (car tab)))
          (check-all-rows (cdr tab) (+ 1 i)))))

(theorem problem-90
         (equal
          (check-all-rows
           (list (list 23  100)
                 (list 1000000 (omega))
                 (list (o^ (omega) 2)
                       (o* (omega) 2))
                 (list (o+ (o* (o^ (omega) 3) 5)
                           (o* (o^ (omega) 1) 25)
                           7)
                       (o+ (o* (o^ (omega) 3) 5)
                           (o* (o^ (omega) 2) 1)
                           3))
                 (list (o+ (o* (o^ (omega) (o^ (omega) 2)) 5)
                           3)
                       (o+ (o* (o^ (omega) (omega)) 5)
                           (o* (o^ (omega) 1) 25)
                           7)))
           1)
;                 a                      b                           answer

          '((1    23                     100                         A<B)
            (2    1000000                ((1 . 1) . 0)               A<B)
            (3    ((2 . 1) . 0)          ((1 . 2) . 0)               B<A)
            (4    ((3 . 5) (1 . 25) . 7) ((3 . 5) (2 . 1) . 3)       A<B)
            (5    ((((2 . 1) . 0) . 5) . 3)
                                         ((((1 . 1) . 0) . 5) (1 . 25) . 7)
                                                                     B<A)))

         :hints (("Goal"
                  :in-theory (enable (omega)
                                     (o^)
                                     (o*)
                                     (o+))))
         :rule-classes nil)

:next-problem #{"""
; ------------------------------------------------------------
; Problem 91.

; Note: If you don't load the ordinals book, you can skip enabling of
; all the functions below!  They're normally enabled.  The book disables
; them so that you can use the algebraic notation and lemmas will fire
; to simplify.  Since I used raw conses to construct my ordinals, I'm
; having to fight the book here.  But by using raw conses, you can
; construct a simple proof without the ordinals book.
"""}

(defun m2 (i j)
  (cons (cons 1 (+ 1 i)) j))

(in-theory (enable o< o+ o* omega (omega)
                   o-first-coeff
                   o-first-expt
                   o-rst
                   o-finp
                   o-p))

(theorem problem-91
  (implies (and (natp i1)
                (natp j1)
                (natp i2)
                (natp j2))
           (and (o-p (m2 i1 j1))
                (iff (o< (m2 i1 j1)
                         (m2 i2 j2))
                     (if (equal i1 i2)
                         (< j1 j2)
                       (< i1 i2)))))
  :rule-classes nil)

:next-problem #{"""
; ------------------------------------------------------------
; Problem 92.

; The longest decreasing chain from 10 has eleven ordinals in it:

; 0 o< 1 o< 2 o< 3 o< 4 o< 5 o< 6 o< 7 o< 8 o< 9 o< 10

; There is no longest decreasing chain from ((1 . 1) . 0).  But any
; step down from that will be a finite natural, e.g., n.  And from n
; down to 0 there can be at most n+1 steps.  So any decreasing chain
; from ((1 . 1) . 0) will have at most n+2 ordinals in it, but n can
; be an arbitrary natural.
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 93.

; The following infinite chain is decreasing.

; x0 ((2 . 1) . 0)
; x1 ((1 . 1) (2 . 1) . 0)
; x2 ((1 . 1) (1 . 1) (2 . 1) . 0) 
; x3 ((1 . 1) (1 . 1) (1 . 1) (2 . 1) . 0) 
;    ...

; That is, ... x3 o< x2 o< x1 o< x0.  But all these objects (except
; x0) fail to be ordinals because the powers of omega do not decrease.
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 94.

; For a proof of the well-foundedness of our ordinals, see the ACL2
; online documentation topic proof-of-well-foundedness:

; http://www.cs.utexas.edu/users/moore/acl2/manuals/latest/index.html?topic=ACL2____PROOF-OF-WELL-FOUNDEDNESS

; Alternatively, go to the ACL2 home page

; http://www.cs.utexas.edu/users/moore/acl2

; and click on
; > The User's Manual
;  > Index of all documented topics
;   > P
;    > PROOF-OF-WELL-FOUNDEDNESS
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 95.

; The measure is cc.  The measure conjecture is
"""}

(theorem problem-95
         (and (o-p (cc x))
              (implies (not (atom x))
                       (o< (cc (first x)) (cc x)))
              (implies (not (atom x))
                       (o< (cc (rest x)) (cc x))))

         :hints (("Goal"
                  :in-theory (enable problem-85)))
         :rule-classes nil)

:----- #{"""
; To admit this definition of tree-copy with the measure cc we would
; write the following and it would generate and prove the conjecture
; above.  

; (defun tree-copy (x)
;   (declare (xargs :measure (cc x)))
;   (if (atom x)
;       x
;     (cons (tree-copy (first x))
;           (tree-copy (rest x)))))

; However we cannot, since tree-copy has already been defined.  For
; the other problems of this sort, we actually define the required
; function and you can look at the ACL2 output to see the measure
; conjectures and their proofs.
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 96.
"""}

(defun ack (x y)
  (declare (xargs :measure (m2 (nfix y) (nfix x))))
  (if (zp x)
      1
    (if (zp y)
        (if (equal x 1) 2 (+ x 2))
      (ack (ack (- x 1) y) (- y 1)))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 97.

; The proof of the existence of non-primitive recursive functions
; has not been carried out in ACL2 but was carried out in the
; closely related Nqthm.  See

; http://www.cs.utexas.edu/users/boyer/ftp/nqthm/nqthm-1992/examples/basic/pr.events
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 98.
"""}

(defun f1 (i j)
  (declare (xargs :measure (if (and (natp i)
                                    (natp j)
                                    (< i j))
                               (- j i)
                             0)))
  (if (and (natp i)
           (natp j)
           (< i j))
      (f1 (+ 1 i) j)
    1))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 99.
"""}

(defun f2 (x)
  (declare (xargs :measure
                  (if (equal x nil)
                      0
                    (+ 1 (cc x)))))
  (if (equal x nil)
      2
    (and (f2 (car x))
         (f2 (cdr x)))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 100.
"""}

(defun f3 (x y)
  (declare (xargs :measure (+ (cc x)
                              (cc y))))
  (if (and (endp x)
           (endp y))
      3
    (f3 (cdr x) (cdr y))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 101.

; I'd like to thank Anand Padmanaban for helping me formulate and
; solve this problem.

; The following mysterious incantation makes ACL2 add a new axiom,
; called problem-101a, that constrains m, p, dn, and up as stated in
; the problem.  For example, dn represents ``down'', and we know
; nothing about (up x).
"""}

(encapsulate ((p (x) t)
              (dn (x) t)  ; dn = ``down''
              (up (x) t)
              (m (x) t))
             (local (defun p (x) (not (zp x))))
             (local (defun dn (x) (- x 1)))
             (local (defun up (x) x))
             (local (defun m (x) (acl2-count x)))
             (theorem problem-101a
               (and (o-p (m x))
                    (implies (p x)
                             (o< (m (dn x)) (m x))))))

(theorem problem-101b
         (implies (p x)
                  (not (equal (m x) 0)))

         :hints (("Goal"
                  :use
                  ((:instance problem-101a (x x))
                   (:instance problem-101a (x (dn x)))))))

(theorem problem-101c
         (or (consp (m x))
             (and (integerp (m x))
                  (<= 0 (m x))))
         :rule-classes :type-prescription

         :hints (("Goal"
                  :use
                  ((:instance problem-101a (x x))
                   (:instance problem-101a (x (dn x)))))))

(theorem problem-101d
         (implies (p x)
                  (not (equal (m (dn x)) (m x))))

         :hints (("Goal"
                  :use
                  ((:instance problem-101a (x x))
                   (:instance problem-101a (x (dn x)))))))

(defun f4 (x y q)
  (declare (xargs :measure (if q
                               (if (equal (m x) 0)
                                   1
                                 (make-ord (m x) 1 1))
                             (if (equal (m y) 0)
                                 2
                               (make-ord (m y) 1 2)))

                  :hints (("Goal"
                           :in-theory (enable problem-101a
                                              problem-101b)))))
  (if (p x)
      (if q
          (f4 y (dn x) (not q))
        (f4 y (up x) (not q)))
    4))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 102.
"""}

(theorem problem-102
         (equal (f1 i j) 1)

         :hints (("Goal"
                  :induct (f1 i j))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 103.
"""}

(theorem problem-103
         (equal (f2 x) 2)

         :hints (("Goal"
                  :induct (f2 x))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 104.
"""}

(theorem problem-104
         (equal (f3 x y) 3)

         :hints (("Goal"
                  :induct (f3 x y))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 105.
"""}

(theorem problem-105
         (equal (f4 x y q) 4)

         :hints (("Goal"
                  :induct (f4 x y q))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 106.
"""}

(defun flatten! (x)
  (declare (xargs :measure (m2 (cc x) (cc (car x)))))
  (if (atom x)
      (cons x nil)
    (if (atom (car x))
        (cons (car x) (flatten! (cdr x)))
      (flatten! (cons (caar x) (cons (cdar x) (cdr x)))))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 107.
"""}

(theorem problem-107
         (equal (flatten! x) (flatten x))

         :hints (("Goal"
                  :induct (flatten! x)
                  :in-theory (enable problem-40))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 108.
"""}

(defun gopher (x)
  (declare (xargs :measure (cc (car x))))
  (if (or (atom x)
          (atom (car x)))
      x
    (gopher (cons (car (car x))
                  (cons (cdr (car x))
                        (cdr x))))))

(theorem problem-108a
         (<= (cc (gopher x)) (cc x))

         :hints (("Goal"
                  :induct (gopher x)))
         :rule-classes :linear)

(theorem problem-108b
         (equal (consp (gopher x))
                (consp x))

         :hints (("Goal"
                  :induct (gopher x))))

(theorem problem-108c
         (implies (consp x)
                  (< (cc (cdr x)) (cc x)))

         :hints (("Goal"
                  :in-theory (enable problem-85)))
         :rule-classes :linear)

(theorem problem-108d
         (implies (consp x)
                  (< (cc (cdr (gopher x))) (cc x)))

         :hints (("Goal"
                  :in-theory (enable problem-108a
                                     problem-108b
                                     problem-108c))))

(defun samefringe (x y)
  (declare (xargs :measure (cc x)

                  :hints (("Goal"
                           :in-theory (enable problem-108d)))))
  (if (or (atom x)
          (atom y))
      (equal x y)
    (and (equal (car (gopher x))
                (car (gopher y)))
         (samefringe (cdr (gopher x))
                     (cdr (gopher y))))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 109.
"""}

(theorem problem-109a
         (equal (car (gopher x))
                (if (consp x)
                    (car (flatten x))
                  nil))

         :hints (("Goal"
                  :induct (gopher x)
                  :in-theory (enable problem-40))))

(theorem problem-109b
         (equal (flatten (cdr (gopher x)))
                (if (consp x)
                    (cdr (flatten x))
                  (cons nil nil)))

         :hints (("Goal"
                  :induct (gopher x)
                  :in-theory (enable problem-40))))

(theorem problem-109c
         (equal (equal (cons e nil) (app x y))
                (if (consp x)
                    (and (equal (car x) e)
                         (atom (cdr x))
                         (equal y nil))
                  (equal y (cons e nil))))

         :hints (("Goal"
                  :induct (app x y))))

(theorem problem-109d
         (equal (equal (flatten x) (cons a nil))
                (and (atom x)
                     (equal x a)))

         :hints (("Goal"
                  :induct (flatten x)
                  :in-theory (enable problem-40
                                     problem-109c))))

(theorem problem-109
         (equal (samefringe x y)
                (equal (flatten x)
                       (flatten y)))

         :hints (("Goal"
                  :induct (samefringe x y)
                  :in-theory (enable problem-109a
                                     problem-109b
                                     problem-109d))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 110.

; McCarthy's idea was that (gopher x) returns a pair (ans . state)
; where ans is the left-most atom in the tree x and state is the state
; of the gopher co-routine.  Thus, if gopher is invoked on state it
; returns the next left-most atom, etc.
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 111.
"""}

(defun rel (fn x y)
  (if (equal fn '<<=)
      (<<= x y)
    (if (equal fn '>>=)
        (<<= y x)
      (if (equal fn '<<)
          (and (<<= x y) (not (equal x y)))
        (and (<<= y x) (not (equal x y)))))))
  
(defun filter (fn x e)
  (cond
   ((endp x) nil)
   ((rel fn (car x) e)
    (cons (car x) (filter fn (cdr x) e)))
   (t (filter fn (cdr x) e))))

(theorem problem-111a
         (<= (cc (filter fn x e)) (cc x))

         :hints (("Goal"
                  :induct (cc x)))
         :rule-classes :linear)

(defun qsort (x)
  (declare (xargs :measure (cc x)))
  (if (endp x)
      nil
    (if (endp (cdr x))
        x
      (app (qsort (filter '<< (cdr x) (car x)))
           (cons (car x)
                 (qsort (filter '>>= (cdr x) (car x))))))))

(theorem problem-111b
         (and (booleanp (perm x y))
              (perm x x)
              (implies (perm x y) (perm y x))
              (implies (and (perm x y) (perm y z))
                       (perm x z)))

         :hints (("Goal"
                  :in-theory (enable problem-53
                                     problem-54
                                     problem-55)))
         :rule-classes (:equivalence))

(theorem problem-111c
         (implies (not (rel fn d e))
                  (equal (filter fn (rm d y) e)
                         (filter fn y e)))

         :hints (("Goal"
                  :induct (filter fn y e))))

(theorem problem-111d
         (equal (mem d (filter fn x e))
                (and (mem d x)
                     (rel fn d e)))

         :hints (("Goal"
                  :induct (len x)
                  :in-theory (enable problem-48
                                     problem-49a))))

(theorem problem-111e
         (implies (not (mem d x))
                  (equal (rm d x) x))

         :hints (("Goal"
                  :induct (rm d x))))

(theorem problem-111f
         (equal (filter fn (rm d x) e)
                (rm d (filter fn x e)))

         :hints (("Goal"
                  :induct (filter fn x e)
                  :in-theory (enable problem-111c
                                     problem-111d
                                     problem-111e))))

(theorem problem-111g
         (implies (perm x y)
                  (perm (filter fn x e)
                        (filter fn y e)))

         :hints (("Goal"
                  :induct (perm x y)
                  :in-theory (enable problem-48
                                     problem-49a
                                     problem-54a
                                     problem-54
                                     problem-55b
                                     problem-55
                                     problem-111b
                                     problem-111d
                                     problem-111e
                                     problem-111f)))
         :rule-classes :congruence)

(theorem problem-111h
         (perm (app a (cons e b))
               (cons e (app a b)))

         :hints (("Goal"
                  :induct (app a b)
                  :in-theory (enable problem-46
                                     problem-54a
                                     problem-54
                                     problem-55
                                     problem-111b))))

(theorem problem-111i
         (perm (app (filter '<< x e)
                    (filter '>>= x e))
               x)

         :hints (("Goal"
                  :induct (filter '>>= x e)
                  :in-theory (enable problem-54a
                                     problem-54
                                     problem-55
                                     problem-111b
                                     problem-111h))))

(theorem problem-111j
         (implies (mem e x)
                  (perm (app (rm e x) y)
                        (rm e (app x y))))

         :hints (("Goal"
                  :induct (app x y)
                  :in-theory (enable problem-53
                                     problem-54
                                     problem-54a
                                     problem-55
                                     problem-111b))))

(theorem problem-111k
         (implies (perm a b)
                  (perm (app a c) (app b c)))

         :hints (("Goal"
                  :induct (perm a b)
                  :in-theory (enable problem-46
                                     problem-48
                                     problem-49a
                                     problem-54a
                                     problem-54
                                     problem-55b
                                     problem-55
                                     problem-111b
                                     problem-111j)))
         :rule-classes :congruence)

(theorem problem-111l
         (implies (perm a b)
                  (perm (app c a) (app c b)))

         :hints (("Goal"
                  :induct (app c b)
                  :in-theory (enable problem-54a
                                     problem-54
                                     problem-55
                                     problem-111b)))
         :rule-classes :congruence)

(theorem problem-111-a
         (perm (qsort x) x)

         :hints (("Goal"
                  :induct (qsort x)
                  :in-theory (enable problem-54
                                     problem-111b
                                     problem-111h
                                     problem-111i
                                     problem-111k
                                     problem-111l))))

(defun all-rel (fn x e)
  (cond ((endp x) t)
        ((rel fn (car x) e)
         (all-rel fn (cdr x) e))
        (t nil)))

(theorem problem-111m
  (equal (car (app a b))
         (if (consp a)
             (car a)
           (car b))))

(theorem problem-111n
         (implies (and (lexorder e (car a))
                       (ordered a))
                  (all-rel '>>= a e))

         :hints (("Goal"
                  :induct (all-rel '>>= a e))))

(theorem problem-111o
         (implies (and (lexorder d (car a))
                       (consp a)
                       (ordered (app a (cons e b))))
                  (lexorder d e))

         :hints (("Goal"
                  :induct (app a (cons e b))
                  :in-theory (enable problem-111m))))

(theorem problem-111p
         (iff (ordered (app a (cons e b)))
              (and (ordered a)
                   (ordered b)
                   (all-rel '<<= a e)
                   (all-rel '>>= b e)))

         :hints (("Goal"
                  :induct (all-rel '<<= a e)
                  :in-theory (enable problem-111m
                                     problem-111n
                                     problem-111o))))

(theorem problem-111q
         (all-rel '<<= (filter '<< x e) e)

         :hints (("Goal"
                  :induct (filter '<< x e))))

(theorem problem-111r
         (all-rel '>>= (filter '>>= x e) e)

         :hints (("Goal"
                  :induct (filter '>>= x e))))

(theorem problem-111s
         (implies (all-rel fn x e)
                  (all-rel fn (rm d x) e))

         :hints (("Goal"
                  :induct (rm d x))))

(theorem problem-111t
         (implies (and (all-rel fn (rm d x) e)
                       (rel fn d e))
                  (all-rel fn x e))

         :hints (("Goal"
                  :induct (all-rel fn x e))))

(theorem problem-111u
         (implies (and (all-rel fn b e) (mem d b))
                  (rel fn d e))

         :hints (("Goal"
                  :induct (mem d b))))

(theorem problem-111v
         (implies (and (rel fn d e) (mem d b))
                  (equal (all-rel fn (rm d b) e)
                         (all-rel fn b e)))

         :hints (("Goal"
                  :induct (all-rel fn b e))))

:----- #{"""
; Note that I disable rel below!
"""}

(theorem problem-111w
         (implies (perm a b)
                  (equal (all-rel fn a e)
                         (all-rel fn b e)))

         :hints (("Goal"
                  :induct (perm a b)
                  :in-theory (e/d (problem-55b
                                   problem-111u
                                   problem-111v)
                                  (rel))))
         :rule-classes :congruence)

(theorem problem-111-b
         (ordered (qsort x))

         :hints (("Goal"
                  :induct (qsort x)
                  :in-theory (enable problem-111p
                                     problem-111q
                                     problem-111r
                                     problem-111w
                                     problem-111-a))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 112.
"""}

(defun no-dups (x)
  (if (endp x)
      t
    (if (mem (car x) (cdr x))
        nil
      (no-dups (cdr x)))))

(defun list-of-natsp (lst)
  (cond ((endp lst) t)
        (t (and (natp (car lst))
                (list-of-natsp (cdr lst))))))

(defun maximal (lst)
  (cond ((endp lst) -1)
        (t (max (car lst)
                (maximal (cdr lst))))))

(theorem problem-112a
         (implies (list-of-natsp lst)
                  (iff (mem (maximal lst) lst)
                       (consp lst)))

         :hints (("Goal"
                  :induct (mem (maximal lst) lst))))

(theorem problem-112b
         (implies (list-of-natsp lst)
                  (list-of-natsp (del e lst)))

         :hints (("Goal"
                  :induct (del e lst))))

(theorem problem-112c
         (implies (no-dups lst)
                  (no-dups (rm e lst)))

         :hints (("Goal"
                  :induct (rm e lst)
                  :in-theory (enable problem-55a
                                     problem-111e))))

(theorem problem-112d
         (implies (list-of-natsp lst)
                  (and (integerp (maximal lst))
                       (<= -1 (maximal lst))))

         :hints (("Goal"
                  :induct (list-of-natsp lst)))
         :rule-classes :forward-chaining)

(theorem problem-112e
         (implies (and (list-of-natsp lst)
                       (no-dups lst)
                       (consp lst))
                  (< (maximal (rm (maximal lst) lst))
                     (maximal lst)))

         :hints (("Goal"
                  :induct (rm (maximal lst) lst)
                  :in-theory (enable problem-112a
                                     problem-112d)))
         :rule-classes :linear)



(theorem problem-112f
         (equal (len (rm e lst))
                (if (mem e lst)
                    (- (len lst) 1)
                  (len lst)))

         :hints (("Goal"
                  :induct (rm e lst)
                  :in-theory (enable problem-111e))))

(defun induction-hint (lst n)
  (declare (xargs :measure (acl2-count n)))
  (cond ((zp n) (list lst n))
        ((endp lst) (list lst n))
        (t (induction-hint (rm (maximal lst) lst) (- n 1)))))

(theorem problem-112g
         (implies (list-of-natsp x)
                  (list-of-natsp (rm e x)))

         :hints (("Goal"
                  :induct (rm e x)
                  :in-theory (enable problem-111e))))

(theorem problem-112h
         (implies (and (consp x)
                       (list-of-natsp x))
                  (<= 0 (maximal x)))

         :hints (("Goal"
                  :induct (list-of-natsp x)))
         :rule-classes :linear)

(theorem problem-112i
         (equal (< 0 (len x))
                (consp x))

         :hints (("Goal"
                  :induct (len x))))

(theorem problem-112j
         (implies (and (natp n)
                       (list-of-natsp lst)
                       (no-dups lst)
                       (< (maximal lst) n))
                  (<= (len lst) n))

         :hints (("Goal"
                  :induct (induction-hint lst n)
                  :in-theory (enable problem-112a
                                     problem-112c
                                     problem-112d
                                     problem-112e
                                     problem-112f
                                     problem-112g
                                     problem-112h
                                     problem-112i))))

(theorem problem-112
         (implies (and (list-of-natsp lst)
                       (no-dups lst))
                  (<= (len lst) (+ 1 (maximal lst))))

         :hints (("Goal"
                  
                  :in-theory (enable problem-112d
                                     problem-112j))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 113.
"""}

(defun addressp (ptr m)
  (and (natp ptr)
       (< ptr (len m))))

(defun inc (x)
  (if (integerp x) (+ 1 x) 'infinite))

(defun len-diff (mem seen)
; How many elements of mem are not in seen?  This basically decreases.
  (if (consp mem)
      (if (mem (car mem) seen)
          (len-diff (cdr mem) seen)
        (+ 1 (len-diff (cdr mem) seen)))
    0))

(theorem problem-113a
         (implies (and (natp n)
                       (< n (len m)))
                  (mem (nth n m) m))

         :hints (("Goal"
                  :induct (nth n m)
                  :in-theory (enable problem-112i))))

(theorem problem-113b
         (<= (len-diff mem (cons ptr seen))
             (len-diff mem seen))

         :hints (("Goal"
                  :induct (len-diff mem (cons ptr seen))
                  :in-theory (enable problem-48
                                     problem-49a)))
         :rule-classes :linear)

(theorem problem-113c
         (implies (and (mem ptr mem)
                       (not (mem ptr seen)))
                  (< (len-diff mem (cons ptr seen))
                     (len-diff mem seen)))

         :hints (("Goal"
                  :induct (len-diff mem seen)
                  :in-theory (enable problem-48
                                     problem-49a
                                     problem-113b)))
         :rule-classes :linear)

(defun deref-cnt (ptr mem seen)
  (declare (xargs :measure (m2 (if (mem ptr mem) 1 2)
                               (len-diff mem seen))

                  :hints (("Goal"
                           :in-theory (enable problem-113a
                                              problem-113c)))))
  (if (addressp ptr mem)
      (if (mem ptr seen)
          'infinite
        (inc (deref-cnt (nth ptr mem) mem (cons ptr seen))))
    0))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 114.
"""}

(defun path (ptr mem seen)
  (declare (xargs :measure (m2 (if (mem ptr mem) 1 2)
                               (len-diff mem seen))

                  :hints (("Goal"
                           :in-theory (enable problem-113a
                                              problem-113c)))))
  (if (addressp ptr mem)
      (if (mem ptr seen)
          'infinite
        (path (nth ptr mem) mem (cons ptr seen)))
    (cons ptr seen)))

(theorem problem-114a
         (equal (deref-cnt ptr mem seen)
                (if (equal (path ptr mem seen) 'infinite)
                    'infinite
                  (- (len (path ptr mem seen)) (+ 1 (len seen)))))

         :hints (("Goal"
                  :induct (path ptr mem seen)
                  :in-theory (enable problem-48
                                     problem-49a))))

(defun addressesp (x mem)
  (if (endp x)
      t
    (and (addressp (car x) mem)
         (addressesp (cdr x) mem))))

(theorem problem-114b
         (implies (and (addressesp x mem)
                       (not (natp e)))
                  (not (mem e x)))

         :hints (("Goal"
                  :induct (mem e x))))

(theorem problem-114c
         (implies (and (addressesp x mem)
                       (>= e (len mem)))
                  (not (mem e x)))

         :hints (("Goal"
                  :induct (mem e x))))

(theorem problem-114d
         (implies (and (no-dups seen)
                       (addressesp seen mem))
                  (no-dups (path ptr mem seen)))

         :hints (("Goal"
                  :induct (path ptr mem seen)
                  :in-theory (enable problem-48
                                     problem-49a
                                     problem-114b
                                     problem-114c))))

(theorem problem-114e
         (implies (sub a b) (sub a (cons e b)))

         :hints (("Goal"
                  
                  :in-theory (enable problem-48a
                                     problem-48
                                     problem-49))))

(theorem problem-114f
         (sub a (app a b))

         :hints (("Goal"
                  :induct (sub a (app a b))
                  :in-theory (enable problem-48a
                                     problem-114e))))

(theorem problem-114g
         (sub b (app a b))

         :hints (("Goal"
                  :induct (app a b)
                  :in-theory (enable problem-48
                                     problem-114e))))

(theorem problem-114h
         (sub (path ptr mem seen)
              (cons ptr (app seen mem)))

         :hints (("Goal"
                  :induct (path ptr mem seen)
                  :in-theory (enable problem-46
                                     problem-48
                                     problem-49
                                     problem-49a
                                     problem-113a
                                     problem-114e
                                     problem-114f))))

(theorem problem-114i
         (implies (and (not (mem e a))
                       (sub a b))
                  (sub a (rm e b)))

         :hints (("Goal"
                  :induct (sub a b)
                  :in-theory (enable problem-48a
                                     problem-55a
                                     problem-55d))))

(theorem problem-114j
         (implies (and (no-dups x)
                       (sub x y))
                  (<= (len x) (len y)))

         :hints (("Goal"
                  :induct (perm x y)
                  :in-theory (enable problem-48a
                                     problem-48
                                     problem-49a
                                     problem-112f
                                     problem-114i)))
         :rule-classes nil)


(theorem problem-114k
         (equal (len (app a b))
                (+ (len a) (len b)))

         :hints (("Goal"
                  :induct (app a b))))

(theorem problem-114l
         (implies (and (addressesp seen mem)
                       (no-dups seen))
                  (<= (len (path ptr mem seen))
                      (+ 1 (len seen) (len mem))))

         :hints (("Goal"
                  :in-theory (enable problem-114d
                                     problem-114h
                                     problem-114k)
                  :use (:instance problem-114j
                                  (x (path ptr mem seen))
                                  (y (cons ptr (app seen mem))))))
         :rule-classes :linear)

(theorem problem-114
         (<= (deref-cnt ptr mem nil) (+ 1 (len mem)))

         :hints (("Goal"
                  :in-theory (enable problem-114a
                                     problem-114l))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 115.
"""}

(defun fib (i)
  (if (zp i)
      0
    (if (equal i 1)
        1
      (+ (fib (- i 1))(fib (- i 2))))))

(defun ffib (i j k)
  (if (zp i)
      j
    (if (equal i 1)
        k
      (ffib (- i 1) k (+ j k)))))

(theorem problem-115a
         (equal (ffib 2 i j) (+ i j))

         :hints (("Goal"
                  :expand (ffib 2 i j))))

(theorem problem-115b
         (implies (and (natp n)
                       (< 0 n)
                       (natp i)
                       (natp j))
                  (equal (ffib n i j) 
                         (+ (* (fib (- n 1)) i)
                            (* (fib n) j))))

         :hints (("Goal"
                  :induct (ffib n i j)
                  :in-theory (enable problem-115a))))

(theorem problem-115
         (equal (ffib n 0 1) (fib n))

         :hints (("Goal"
                  :in-theory (enable problem-115b)
                  :cases ((zp n)))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 116.
"""}

(defun rot (x)
  (if (endp x)
      nil
    (app (cdr x) (list (car x)))))

(defun rotn (n x)
  (if (zp n) x (rotn (- n 1) (rot x))))

(theorem problem-116-counterexample
  (not (equal (rotn (len '(1 2 3 . 4)) '(1 2 3 . 4))
              '(1 2 3 . 4)))
  :rule-classes nil)

(defun rot-hint (x y)
  (if (consp x)
      (rot-hint (cdr x)
                (app y (cons (car x) nil)))
    y))

(theorem problem-116a
         (implies (and (proper x)
                       (proper y))
                  (equal (rotn (len x) (app x y))
                         (app y x)))

         :hints (("Goal"
                  :induct (rot-hint x y)
                  :in-theory (enable problem-40
                                     problem-41
                                     problem-44c)))
         :rule-classes nil)

(theorem problem-116
         (implies (proper x)
                  (equal (rotn (len x) x) x))

         :hints (("Goal"
                  
                  :in-theory (enable problem-41)
                  :use (:instance problem-116a (x x) (y nil)))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 117.
"""}

(defun n (v)
  (cond ((endp v) 0)
        ((car v) (+ 1 (* 2 (n (cdr v)))))
        (t (* 2 (n (cdr v))))))

(defun band (p q) (if p (if q t nil) nil))
(defun bnot (p)   (if p nil t))
(defun bor  (p q) (if p t (if q t nil)))
(defun bxor (p q) (if p (if q nil t) (if q t nil)))
(defun bmaj (p q c)
  (bor (band p q)
       (bor (band p c)
            (band q c))))

(defun vadd1 (x y c)
  (if (endp x)
      (cons c nil)
    (cons (bxor (car x) (bxor (car y) c))
          (vadd1 (cdr x) (cdr y)
                 (bmaj (car x) (car y) c)))))

(theorem problem-117a
         (equal (equal (len x) 0)
                (not (consp x)))

         :hints (("Goal"
                  :induct (len x))))

(theorem problem-117b
         (implies (equal (len x) (len y))
                  (equal (n (vadd1 x y c))
                         (+ (n x) (n y) (if c 1 0))))

         :hints (("Goal"
                  :induct (vadd1 x y c)
                  :in-theory (enable problem-117a))))

(defun vadd (x y)
  (vadd1 x y nil))

(theorem problem-117
         (implies (equal (len x) (len y))
                  (equal (n (vadd x y))
                         (+ (n x) (n y))))

         :hints (("Goal"
                  :in-theory (enable problem-117b))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 118.

; This problem supposes we have two mutually recursive equations.
; To get mutually recursive definitions admitted into ACL2, we
; use this form:
"""}

(mutual-recursion
 (defun fx (x)
   (if (consp x)
       (cons (fx (car x))
             (gx (cdr x)))
     x))

 (defun gx (x)
   (if (consp x)
       (cons (gx (car x))
             (fx (cdr x)))
     x))
 )

(defun tree-copy (x)
  (if (consp x)
      (cons (tree-copy (car x))
            (tree-copy (cdr x)))
    x))

(theorem problem-118
         (and (equal (fx x) x)
              (equal (gx x) x))

         :hints (("Goal"
                  :induct (tree-copy x))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 119.

; This problem calls for us to develop a methodology for introducing
; mutually recursive functions and to use it to introduce fx and gx
; above.  But to solve the previous problem we introduced the names fx
; and gx and cannot re-introduce them.  So we will demonstrate our
; methodology to introduce a renamed pair of functions:

; (mutual-recursion
;  (defun fz (x)
;    (if (consp x)
;        (cons (fz (car x))
;              (gz (cdr x)))
;      x))
; 
;  (defun gz (x)
;    (if (consp x)
;        (cons (gz (car x))
;              (fz (cdr x)))
;      x))
;  )

; Step 1 of the methodology is to introduce a singly recursive
; function that has a flag argument that determines which of the
; mutually recursive functions it is supposed to compute.
; When fn is 'fz it computes fz; otherwise it computes gz.
"""}

(defun fzgz (fn x)
  (if (equal fn 'fz)
      (if (consp x)
          (cons (fzgz 'fz (car x))
                (fzgz 'gz (cdr x)))
        x)
      (if (consp x)
          (cons (fzgz 'gz (car x))
                (fzgz 'fz (cdr x)))
        x)))

:----- #{"""
; Step 2 is to define the individual functions using the singly
; recursive function.
"""}

(defun fz (x) (fzgz 'fz x))
(defun gz (x) (fzgz 'gz x))

:----- #{"""
; Step 3 is to prove that fz and gz each satisfy the desired
; equations.
"""}

(theorem problem-119-a
  (equal (fz x)
         (if (consp x)
             (cons (fz (car x))
                   (gz (cdr x)))
           x))
  :rule-classes nil)

(theorem problem-119-b
  (equal (gz x)
         (if (consp x)
             (cons (gz (car x))
                   (fz (cdr x)))
           x))
  :rule-classes nil)

:----- #{"""
; Note that we could now behave as though those equations had
; been added as definitional axioms rather than theorems and
; we could simply ignore the earlier definitions of fz and gz.
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 120.
"""}

(defun expr-fn (fn x)
  (if (equal fn 'expr)
      (if (atom x)
          (symbolp x)
        (and (symbolp (car x))
             (expr-fn 'list (cdr x))))
    (if (atom x)
        (equal x nil)
      (and (expr-fn 'expr (car x))
           (expr-fn 'list (cdr x))))))

(defun expr (x) (expr-fn 'expr x))

(defun expr-list (x) (expr-fn 'list x))

(theorem problem-120-a
  (equal (expr x)
         (if (atom x)
             (symbolp x)
           (and (symbolp (car x))
                (expr-list (cdr x)))))
  :rule-classes nil)

(theorem problem-120-b
  (equal (expr-list x)
         (if (atom x)
             (equal x nil)
           (and (expr (car x))
                (expr-list (cdr x)))))
  :rule-classes nil)


:next-problem #{"""
; ------------------------------------------------------------
; Problem 121.
"""}

(defun substitution (s)
  (if (endp s)
      (equal s nil)
    (and (true-listp (car s))
         (equal (len (car s)) 2)
         (symbolp (car (car s)))
         (expr (car (cdr (car s))))
         (substitution (cdr s)))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 122.
"""}

(defun lookup (var alist)
  (if (endp alist)
      var
    (if (equal var (car (car alist)))
        (car (cdr (car alist)))
      (lookup var (cdr alist)))))

(defun slash-fn (fn x s)
  (if (equal fn 'expr)
      (if (atom x)
          (lookup x s)
        (cons (car x) (slash-fn 'list (cdr x) s)))
    (if (atom x)
        nil
      (cons (slash-fn 'expr (car x) s)
            (slash-fn 'list (cdr x) s)))))

(defun slash (x s) (slash-fn 'expr x s))
(defun slash-list (lst s) (slash-fn 'list lst s))


(theorem problem-122-a
  (equal (slash x s)
         (if (atom x)
             (lookup x s)
           (cons (car x) (slash-list (cdr x) s))))
  :rule-classes nil)

(theorem problem-122-b
  (equal (slash-list lst s)
         (if (atom lst)
             nil
           (cons (slash (car lst) s)
                 (slash-list (cdr lst) s))))
  :rule-classes nil)

:next-problem #{"""
; ------------------------------------------------------------
; Problem 123.
"""}

(theorem problem-123a
         (implies (and (symbolp x)
                       (substitution s))
                  (expr-fn 'expr (lookup x s)))

         :hints (("Goal"
                  :induct (lookup x s))))

(theorem problem-123b
         (implies (and (expr-fn fn x)
                       (substitution s))
                  (expr-fn fn (slash-fn fn x s)))

         :hints (("Goal"
                  :induct (slash-fn fn x s)
                  :in-theory (enable problem-123a))))

(theorem problem-123
         (implies (and (expr x)
                       (substitution s))
                  (expr (slash x s)))

         :hints (("Goal"
                  :in-theory (enable problem-123b))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 124.

; The definition of f5 cannot be admitted because of the recursive
; call (f5 (f5 (- x 1))).  We can prove that a measure of the argument
; decreases in the inner recursive call.  (The measure would be cc.)
; But we cannot prove that ANY measure decreases in the outer
; recursive call, because the actual is (f5 (- x 1)) and we do not
; have ANY axiom about f5 yet.
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 125.

; The nested recursion in mcflatten is admissible because it occurs in
; an argument position that is not being measured.  We admit mcflatten
; by measuring the first argument, x.  We do not care what term is in
; the second position, a.

; The nested recursion in ack is more problematic but still
; acceptable.  Recall why ack terminates: either the second argument,
; y, decreases or else the second argument stays fixed and the first,
; x, decreases.  Note that when y decreases, we don't care what x
; does.  So if x is occupied by a nested recursive call, it is ok.
"""}

:next-problem #{"""
; ------------------------------------------------------------
; Problem 126.
"""}

(defun f5 (x)
  (declare (xargs :measure (nfix x)))
  (if (zp x)
      0
    (if (< (nfix (f5 (- x 1))) (nfix x))
        (+ 1 (f5 (f5 (- x 1))))
      'undef)))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 127.
"""}

(theorem problem-127
         (implies (natp x) (<= (f5 x) x))

         :hints (("Goal"
                  :induct (f5 x)))
         :rule-classes :linear)

:next-problem #{"""
; ------------------------------------------------------------
; Problem 128.
"""}

(theorem problem-128
         (equal (f5 x)
                (if (zp x)
                    0
                  (+ 1 (f5 (f5 (- x 1))))))

         :hints (("Goal"
                  :in-theory (enable problem-127)))
         :rule-classes nil)

:next-problem #{"""
; ------------------------------------------------------------
; Problem 129.
"""}

(defun flatten-m (x)
  (if (consp x)
      (if (consp (car x))
          (cons (car (car x))
                (cons (cdr (car x))
                      (flatten-m (cdr x))))
        (cons (car x) (flatten-m (cdr x))))
    nil))

(theorem problem-129a
         (implies (and (natp ptr)
                       (< ptr (len g))
                       (consp (nth ptr g)))
                  (mem (car (nth ptr g)) (flatten-m g)))

         :hints (("Goal"
                  :induct (nth ptr g)
                  :in-theory (enable problem-48
                                     problem-49a
                                     problem-112i
                                     problem-114e))))

(theorem problem-129b
         (implies (and (natp ptr)
                       (< ptr (len g))
                       (consp (nth ptr g)))
                  (mem (cdr (nth ptr g)) (flatten-m g)))

         :hints (("Goal"
                  :induct (nth ptr g)
                  :in-theory (enable problem-48
                                     problem-49a
                                     problem-112i
                                     problem-114e))))

(theorem problem-129c
         (implies (and (natp ptr)
                       (< ptr (len g))
                       (not (consp (nth ptr g))))
                  (mem (nth ptr g) (flatten-m g)))

         :hints (("Goal"
                  :induct (nth ptr g)
                  :in-theory (enable problem-48
                                     problem-49a
                                     problem-112i
                                     problem-114e))))

(theorem problem-129d
         (implies (sub seen1 seen2)
                  (<= (len-diff x seen2)
                      (len-diff x seen1)))

         :hints (("Goal"
                  :induct (len-diff x seen2)
                  :in-theory (enable problem-48
                                     problem-49a)))
         :rule-classes :linear)

(theorem problem-129e
         (implies (and (not (mem ptr seen1))
                       (mem ptr seen2)
                       (sub seen1 seen2)
                       (mem ptr x))
                  (< (len-diff x seen2)
                     (len-diff x seen1)))

         :hints (("Goal"
                  :induct (len-diff x seen1)
                  :in-theory (enable problem-48
                                     problem-49
                                     problem-49a
                                     problem-129d)))
         :rule-classes :linear)

(defun reachables (ptr m seen)
  (declare (xargs :measure (m2 (if (mem ptr (flatten-m m)) 1 2)
                               (len-diff (flatten-m m) seen))

                  :hints (("Goal"
                           :in-theory (enable problem-48
                                              problem-114e
                                              problem-129a
                                              problem-129b
                                              problem-129c
                                              problem-129e)))))
  (if (addressp ptr m)
      (if (mem ptr seen)
          seen
        (if (consp (nth ptr m))
            (if (sub (cons ptr seen)
                     (reachables (cdr (nth ptr m))
                                 m
                                 (cons ptr seen)))
                (reachables (car (nth ptr m))
                            m
                            (reachables (cdr (nth ptr m))
                                        m
                                        (cons ptr seen)))
              'undef)
          (reachables (nth ptr m) m (cons ptr seen))))
    seen))

:----- #{"""
; This is the key fact about reachables: it doesn't unmark any nodes!
"""}

(theorem problem-129f
         (sub seen (reachables ptr m seen))

         :hints (("Goal"
                  :induct (reachables ptr m seen)
                  :in-theory (enable problem-48
                                     problem-49
                                     problem-49a)))
         :rule-classes nil)

(theorem problem-129g
         (sub (cons ptr seen)
              (reachables (cdr (nth ptr m))
                          m
                          (cons ptr seen)))

         :hints (("Goal"
                  :use (:instance problem-129f
                                  (ptr (cdr (nth ptr m)))
                                  (m m)
                                  (seen (cons ptr seen))))))

(theorem problem-129
         (equal (reachables ptr m seen)
                (if (addressp ptr m)
                    (if (mem ptr seen)
                        seen
                      (if (consp (nth ptr m))
                          (reachables (car (nth ptr m))
                                      m
                                      (reachables (cdr (nth ptr m))
                                                  m
                                                  (cons ptr seen)))
                        (reachables (nth ptr m) m (cons ptr seen))))
                  seen))

         :hints (("Goal"
                  :in-theory (enable problem-129g)))
         :rule-classes nil)

:next-problem #{"""
; ------------------------------------------------------------
; Problem 130.
"""}

(defun rmb (x)
  (declare (xargs :measure (cc x)))
  (if (consp x)
      (if (consp (cdr x))
          (if (< (cc (cdr (rmb (cdr x))))
                 (cc x))
              (if (< (cc (cons (car x)
                               (rmb (cdr (rmb (cdr x))))))
                     (cc x))
                  (cons (car (rmb (cdr x)))
                        (rmb (cons (car x)
                                   (rmb (cdr (rmb (cdr x)))))))
                'undef)
            'undef)
        (cons (car x) nil))
    nil))

(theorem problem-130a
  (<= (cc (cdr x)) (cc x))
  :rule-classes :linear)

(theorem problem-130b
         (<= (cc (rmb x)) (cc x))

         :hints (("Goal"
                  :induct (rmb x)))
         :rule-classes :linear)

(theorem problem-130c
         (implies (consp x)
                  (consp (rmb x)))

         :hints (("Goal"
                  :induct (rmb x)
                  :in-theory (enable problem-108c
                                     problem-130a
                                     problem-130b))))

(theorem problem-130
         (equal (rmb x)
                (if (consp x)
                    (if (consp (cdr x))
                        (cons (car (rmb (cdr x)))
                              (rmb (cons (car x)
                                         (rmb (cdr (rmb (cdr x)))))))
                      (cons (car x) nil))
                  nil))

         :hints (("Goal"
                  
                  :in-theory (enable problem-108c
                                     problem-130b
                                     problem-130c)))
         :rule-classes ((:definition :controller-alist ((rmb t)))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 131.

; Basically, just use the facts we already know about app and rev,
; plus induction hypotheses that the rmb calls are rev calls,
; to prove the theorem.  The proof requires some
; knowledge of proper lists, since our lemmas about app and rev
; involve that concept.  In particular, we need:
"""}

(theorem problem-131a
  (equal (proper (cdr x))
         (or (atom x)
             (proper x))))

:----- #{"""
; Informally, that's enough to do the proof if you could just
; do an induction to unwind rmb.  But we haven't proved the
; measure conjectures about the rmb recursion.  Rather than
; try that, we take a nice short cut.  Since we are going to
; be proving that rmb is rev, we will prove the measure conjectures
; about the rmb recursion -- but we'll substitute rev calls for
; each rmb call.  That is what the hint below does.  We need
; a few lemmas.
"""}

(theorem problem-131b
         (<= (cc (app a b))
             (+ (cc a)
                (cc b)))

         :hints (("Goal"
                  :induct (cc a)))
         :rule-classes :linear)

(theorem problem-131c
         (<= (cc (rev x))
             (cc x))

         :hints (("Goal"
                  :induct (cc x)
                  :in-theory (enable problem-131b)))
         :rule-classes :linear)
           
(theorem problem-131d
         (equal (consp (rev x))
                (consp x))

         :hints (("Goal"
                  :induct (rev x))))

(defun rmb-hint (x)
  (declare (xargs :measure (cc x)

                  :hints (("Goal"
                           :in-theory (enable problem-108c
                                              problem-130a
                                              problem-131c
                                              problem-131d)))))
  (if (consp x)
      (if (consp (cdr x))
          (list (rmb-hint (cdr x))
                (rmb-hint (cdr (rev (cdr x))))
                (rmb-hint (cons (car x)
                                (rev (cdr (rev (cdr x)))))))
        x)
    x))

(theorem problem-131
         (equal (rmb x) (rev x))
         :hints (("Goal"
                  :induct (rmb-hint x)
                  :in-theory (enable problem-44b
                                     problem-44
                                     problem-130
                                     problem-131a
                                     problem-131d))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 132.
"""}

(defun if-exprp (x)
  (and (consp x)
       (equal (car x) 'if)))

(defun a1 (x) (cadr x))
(defun a2 (x) (caddr x))
(defun a3 (x) (cadddr x))

:----- #{"""
; In ACL2, (ASSOC-EQUAL x alist) finds the first pair in alist whose
; car is equal to x.  We use it below.
"""}

(defun assignment (var alist)
  (if (quotep var)
      (car (cdr var)) ; var = (QUOTE val)
      (cdr (assoc-equal var alist))))

:----- #{"""
; We can't call our evaluator eval because that is a pre-defined
; Common Lisp function.  We use peval instead; it stands for
; ``propositional evaluator.''
"""}

(defun peval (x alist)
  (declare (xargs :measure (cc x)))
  (cond ((if-exprp x)
         (if (peval (a1 x) alist)
             (peval (a2 x) alist)
           (peval (a3 x) alist)))
        (t (assignment x alist))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 133.

; Here is the definition of IF-normal form:
"""}

(defun normp (x)
  (declare (xargs :measure (cc x)))
  (if (if-exprp x)
      (and (not (if-exprp (a1 x)))
           (normp (a2 x))
           (normp (a3 x)))
    t))

:----- #{"""
; To admit norm, we need some measures.
"""}

(defun if-depth (x)
  (declare (xargs :measure (cc x)))
  (if (if-exprp x)
      (+ 1 (if-depth (a1 x)))
    0))

(defun if-complexity (x)
  (declare (xargs :measure (cc x)))
  (if (if-exprp x)
      (* (if-complexity (a1 x))
         (+ (if-complexity (a2 x))
            (if-complexity (a3 x))))
    1))

(theorem problem-133a
         (<= 1 (if-complexity x))
         :hints (("Goal" :induct (if-complexity x)))
         :rule-classes :linear)

(theorem problem-133b
         (implies (and (rationalp x)
                       (rationalp y)
                       (<= 1 x)
                       (< 0 y))
                  (<= y (* x y)))
         :rule-classes :linear)

(theorem problem-133c
         (implies (if-exprp x)
                  (< (if-complexity (a2 x))
                     (if-complexity x)))
         :hints (("Goal"
                  :induct (if-complexity x)
                  :in-theory (enable problem-133b)))
         :rule-classes :linear)

(theorem problem-133d
         (implies (if-exprp x)
                  (< (if-complexity
                      (a3 x))
                     (if-complexity x)))
         :hints (("Goal"
                  :induct (if-complexity x)
                  :in-theory (enable problem-133b)))
         :rule-classes :linear)

(defun norm (x)
  (declare (xargs :measure (m2 (if-complexity x) (if-depth x))
                  :hints (("Goal" :in-theory (enable problem-133a
                                                     problem-133c
                                                     problem-133d)))))
  (cond ((not (if-exprp x)) x)
        ((if-exprp (a1 x))
         (norm (list 'if (a1 (a1 x))
                     (list 'if
                           (a2 (a1 x))
                           (a2 x)
                           (a3 x))
                     (list 'if
                           (a3 (a1 x))
                           (a2 x)
                           (a3 x)))))
        (t (list 'if (a1 x)
                 (norm (a2 x))
                 (norm (a3 x))))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 134.
"""}

(defun assignedp (var alist)
   (or (quotep var)
       (assoc-equal var alist)))

(defun assume-true (var alist)
   (cons (cons var t)
         alist))

(defun assume-false (var alist)
  (cons (cons var nil)
        alist))

(defun tautp (x alist)
  (declare (xargs :measure (cc x)))
  (if (if-exprp x)
      (if (assignedp (a1 x) alist)
          (if (assignment (a1 x) alist)
              (tautp (a2 x) alist)
            (tautp (a3 x) alist))
        (and (tautp (a2 x)
                    (assume-true (a1 x) alist))
             (tautp (a3 x)
                    (assume-false (a1 x) alist))))
    (assignment x alist)))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 135.
"""}

(defun tautology-checker (x)
   (tautp (norm x) nil))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 136.
"""}

(theorem problem-136a
         (implies (alistp a)
                  (equal (assoc-equal x (app a b))
                         (if (assoc-equal x a)
                             (assoc-equal x a)
                           (assoc-equal x b))))
         :hints (("Goal" :induct (app a b))))

(theorem problem-136b
         (implies (iff (cdr (assoc-equal var alist)) val)
                  (iff (peval x (cons (cons var val) alist))
                       (peval x alist)))
         :hints (("Goal" :induct (peval x alist))))

(theorem problem-136c
         (implies (and (alistp a)
                       (normp x)
                       (tautp x a))
                  (peval x (app a b)))
         :hints (("Goal"
                  :induct (tautp x a)
                  :in-theory (enable problem-136a
                                     problem-136b))))
  
(theorem problem-136d
         (normp (norm x))
         :hints (("Goal" :induct (norm x))))

(theorem problem-136e
         (equal (peval (norm x) a)
                (peval x a))
         :hints (("Goal" :induct (norm x))))

(theorem problem-136
         (implies (tautology-checker x)
                  (peval x a))
         :hints (("Goal"
                  :in-theory (enable problem-136d
                                     problem-136e)
                  :use (:instance problem-136c
                                  (a nil)
                                  (b a)
                                  (x (norm x))))))

:next-problem #{"""
; ------------------------------------------------------------
; Problem 137.

; Below we use two ACL2 language features not previously used in this
; material, mv and mv-let.  (mv a b) returns a vector (list) of length
; 2 containing a and b.  (mv-let (x y) <foo> <bar>) evaluates <foo>,
; obtaining a list of length 2, binds x and y to the to elements, and
; then evaluates <bar>.  Thus,
; (mv a b)
; is the same as
; (cons a (cons b nil))
; and
; (mv-let (x y) <foo> <bar>)
; is the same as
; ((lambda (vector)
;   ((lambda (x y)
;     <bar>)
;    (nth 0 vector)
;    (nth 1 vector)))
;  <foo>)
; However, if mv and mv-let are used instead of the expressions
; above, the syntax checker in ACL2 insures that <foo> really does
; produce a vector of length 2.  In addition, mv and mv-let are more
; efficient than the expressions above, because they do not actually
; create the vector.
"""}

(defun falsify (x alist)
  (declare (xargs :measure (cc x)))
  (if (if-exprp x)
      (if (assignedp (a1 x) alist)
          (if (assignment (a1 x) alist)
              (falsify (a2 x) alist)
            (falsify (a3 x) alist))
        (mv-let (ans new-alist)
                (falsify (a2 x)
                         (assume-true (a1 x) alist))
                (if ans
                    (mv ans new-alist)
                  (falsify (a3 x)
                           (assume-false (a1 x) alist)))))
    (if (assignedp x alist)
        (if (assignment x alist)
            (mv nil nil)
          (mv t alist))
      (mv t (assume-false x alist)))))

(defun falsifying-alist (x)
  (mv-let (ans alist)
          (falsify (norm x) nil)
          (declare (ignore ans))
          alist))

:----- #{"""
; For reasons having to do with the syntactic checking noted above,
; ACL2 accesses the components of the vector with mv-nth rather than
; nth.  Logically, mv-nth is nth.
"""}

(theorem problem-137a
         (implies (and (normp x)
                       (not (tautp x a)))
                  (mv-nth 0 (falsify x a)))
         :hints (("Goal" :induct (falsify x a))))

(theorem problem-137b
         (implies (assoc-equal var a)
                  (equal (cdr (assoc-equal var (mv-nth 1 (falsify x a))))
                         (if (mv-nth 0 (falsify x a))
                             (cdr (assoc-equal var a))
                           nil)))
         :hints (("Goal" :induct (falsify x a))))

(theorem problem-137c
         (implies (and (mv-nth 0 (falsify x a))
                       (normp x))
                  (not (peval x (mv-nth 1 (falsify x a)))))
         :hints (("Goal"
                  :induct (falsify x a)
                  :in-theory (enable problem-137b))))

(theorem problem-137
         (implies (not (tautology-checker x))
                  (not (peval x (falsifying-alist x))))
         :hints (("Goal"
                  :in-theory (enable problem-136d
                                     problem-136e
                                     problem-137a)
                  :use (:instance problem-137c
                                  (a nil)
                                  (x (norm x))))))