;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; In an unpublished paper, Textbook Examples of Recursion, Donald E.
; Knuth of Stanford University gives the following generalization of
; McCarthy's 91 function:
; Let a be a real, let b and d be positive reals, and let c be a
; positive integer.
; Define K( x ) for integer inputs x by
;   K( x ) <== if  x > a  then  x - b
;                         else  K( ... K( x+d ) ... ).
; Here the else-clause in this definition has c applications of the
; function K.
; When a = 100, b = 10, c = 2, and d = 11, the definition specializes
; to McCarthy's original 91 function:
;   K( x ) <== if  x > 100  then  x - 10
;                           else  K( K( x+11 ) ).
; Knuth calls the first definition of K given above, the generalized
; 91 recursion scheme with parameters ( a,b,c,d ).
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; The purpose of this file of Boyer-Moore-Kaufmann events is to
; provide mechanical verification of the following theorem given by
; Knuth in his paper.
; Theorem.  The generalized 91 recursion with parameters ( a,b,c,d )
;           defines a total function on the integers if and only if
;           (c-1)b < d.  In such a case the values of K( x ) also
;           satisfy the much simpler recurrence
;           K( x )  =  if  x > a  then  x - b
;                                 else  K( x+d-(c-1)b ).
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Use the library of integer facts.

Event: Start with the library "integers".

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Introduce a new function FN of one argument with
;  no constraints.

Conservative Axiom: fn-intro t

Simultaneously, we introduce the new function symbol fn.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Recursively define what it means to
; iterate applications of FN.

Definition: iter-fn (i, x) = if i ≃ 0 then x

else fn (iter-fn (i − 1, x)) endif

Theorem: iter-fn=fn iter-fn (1, x) = fn (x)

Theorem: iter-fn-sum iter-fn (i, iter-fn (j , x)) = iter-fn (i + j , x)

Theorem: iter-fn-sum-integer (ilessp (0, i) ∧ ilessp (0, j )) → (iter-fn (i, iter-fn (j , x)) = iter-fn (iplus (i, j ), x))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Introduce new constants (ie., functions with no arguments)
;  P, Q, R, and S with the indicated constaints

Conservative Axiom: p-q-r-s-intro integerp (p) ∧ integerp (q) ∧ integerp (r) ∧ integerp (s) ∧ (¬ ilessp (q, 0)) ∧ (¬ ilessp (p, s))

Simultaneously, we introduce the new function symbols p, q, r, and s.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Define a "general Knuth" function, GK, of one argument
;  which will be used later to help witness the existence
;  of functions which satisfy the defining recursion of
;  the generalized 91 function.

Definition: k-measure (a, x) = if ilessp (a, x) then 0

else iplus (1, iplus (a, ineg (x))) endif

Theorem: k-measure-returns-numberp k-measure (a, x) ∈ N

Theorem: k-measure-x+y<k-measure-y ((¬ ilessp (a, y)) ∧ ilessp (0, x)) → (k-measure (a, iplus (x, y)) < k-measure (a, y))

Event: Disable k-measure.

Definition: gk (x) = if ilessp (p, x) then iplus (x, ineg (q))

elseif ilessp (0, r) then gk (iplus (r, x))

else s endif

Definition: iter-gk (i, x) = if i ≃ 0 then x

else gk (iter-gk (i − 1, x)) endif

Theorem: iter-gk=gk iter-gk (1, x) = gk (x)

Theorem: itergk-x=itergk-x+r ((0 < i) ∧ ilessp (0, r) ∧ (¬ ilessp (p, x))) → (iter-gk (i, x) = iter-gk (i, iplus (r, x)))

Theorem: count x-1<count x (ilessp (0, x) ∧ (x ≠ 1)) → (count (iplus (-1, x)) < count (x))

Definition: induct-hint-pos-int (x) = if ¬ ilessp (0, x) then t

elseif x = 1 then t

else induct-hint-pos-int (iplus (-1, x)) endif

Theorem: n-1>0-when-n>0&n<>1 (ilessp (0, n) ∧ (n ≠ 1)) → ilessp (0, iplus (-1, n))

Theorem: x<=z-when-x<y&y<=z (ilessp (x, y) ∧ (¬ ilessp (z, y))) → (¬ ilessp (z, x))

Theorem: x+ n-1 r<x+nr-when-0<r ilessp (0, r) → ilessp (iplus (x, itimes (iplus (-1, n), r)), iplus (x, itimes (n, r)))

Theorem: p+r>=x+ n-1 r-when-p+r>=x+nr (ilessp (0, r) ∧ (¬ ilessp (iplus (p, r), iplus (x, itimes (n, r))))) → (¬ ilessp (iplus (p, r), iplus (x, itimes (iplus (-1, n), r))))

Theorem: x>=y-z-when-x+z>=y (¬ ilessp (iplus (x, z), y)) → (¬ ilessp (x, iplus (y, ineg (z))))

Theorem: itergk-x=itergk-x+nr-induction-step (ilessp (0, n) ∧ (n ≠ 1) ∧ (((0 < i)

∧ ilessp (0, r)

∧ ilessp (0, iplus (-1, n))

∧ (¬ ilessp (iplus (p, r), iplus (x, itimes (iplus (-1, n), r))))) → (iter-gk (i, x) = iter-gk (i, iplus (x, itimes (iplus (-1, n), r)))))

∧ (0 < i) ∧ ilessp (0, r) ∧ (¬ ilessp (iplus (p, r), iplus (x, itimes (n, r))))) → ((iter-gk (i, x) = iter-gk (i, iplus (x, itimes (r, n)))) = t)

Theorem: itergk-x=itergk-x+nr ((0 < i) ∧ ilessp (0, r) ∧ ilessp (0, n) ∧ (¬ ilessp (iplus (p, r), iplus (x, itimes (n, r))))) → (iter-gk (i, x) = iter-gk (i, iplus (x, itimes (n, r))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Define the function N( a,d,x ) recursively,
;  so that whenever d > 0, N( a,d,x ) is the smallest
;  nonnegative integer i such that x + id > a.

Definition: n (a, d, x) = if ¬ ilessp (0, d) then 0

elseif ilessp (a, x) then 0

else iplus (1, n (a, d, iplus (x, d))) endif

Theorem: n>=0 ¬ ilessp (n (a, d, x), 0)

Theorem: n>0-when-d>o&x<=a (ilessp (0, d) ∧ (¬ ilessp (a, x))) → ilessp (0, n (a, d, x))

Theorem: a<x+nd ilessp (0, d) → ilessp (a, iplus (x, itimes (n (a, d, x), d)))

Theorem: a+d>=x+nd-when-d>0&a>=x (ilessp (0, d) ∧ (¬ ilessp (a, x))) → (¬ ilessp (iplus (a, d), iplus (x, itimes (n (a, d, x), d))))

Theorem: itergk i x=itergk i-1 x-q+nr-step-1 ((0 < i) ∧ ilessp (0, r) ∧ (¬ ilessp (p, x))) → (iter-gk (i, x) = iter-gk (i, iplus (x, itimes (r, n (p, r, x)))))

Theorem: itergk i x=itergk i-1 x-q+nr-step-2 (0 < i) → (iter-gk (i, iplus (x, itimes (r, n (p, r, x))))

= iter-gk (i − 1, gk (iplus (x, itimes (r, n (p, r, x))))))

Theorem: itergk i x=itergk i-1 x-q+nr-step-3 ((0 < i) ∧ ilessp (0, r) ∧ (¬ ilessp (p, x))) → (iter-gk (i − 1, gk (iplus (x, itimes (r, n (p, r, x)))))

= iter-gk (i − 1, iplus (x, iplus (ineg (q), itimes (r, n (p, r, x))))))

Theorem: itergk i x=itergk i-1 x-q+nr ((0 < i) ∧ ilessp (0, r) ∧ (¬ ilessp (p, x))) → (iter-gk (i, x)

= iter-gk (i − 1, iplus (x, iplus (ineg (q), itimes (r, n (p, r, x))))))

Theorem: x>=z-when-x>=y&y>=z ((¬ ilessp (x, y)) ∧ (¬ ilessp (y, z))) → (¬ ilessp (x, z))

Theorem: x+y>=x+-z+y-when-z>=0 (¬ ilessp (z, 0)) → (¬ ilessp (iplus (x, y), iplus (iplus (x, ineg (z)), y)))

Theorem: itergk i-1 x-q=itergk i-1 x-q+nr ((1 < i) ∧ ilessp (0, r) ∧ (¬ ilessp (p, x))) → (iter-gk (i − 1, iplus (x, ineg (q)))

= iter-gk (i − 1, iplus (x, iplus (ineg (q), itimes (r, n (p, r, x))))))

Theorem: itergk i x=itergk i-1 x-q-when-p>=x&r>0 ((1 < i) ∧ ilessp (0, r) ∧ (¬ ilessp (p, x))) → (iter-gk (i, x) = iter-gk (i − 1, iplus (x, ineg (q))))

Theorem: itergk=s-when-p>=x&0>=r&0<i ((0 < i) ∧ (¬ ilessp (0, r)) ∧ (¬ ilessp (p, x))) → (iter-gk (i, x) = s)

Theorem: x>=x+-y-when-y>=0 (¬ ilessp (y, 0)) → (¬ ilessp (x, iplus (x, ineg (y))))

Theorem: itergk i x=itergk i-1 x-q-when-p>=x&0>=r ((1 < i) ∧ (¬ ilessp (0, r)) ∧ (¬ ilessp (p, x))) → (iter-gk (i, x) = iter-gk (i − 1, iplus (x, ineg (q))))

Theorem: itergk i x=itergk i-1 x-q-when-p<x ((0 < i) ∧ ilessp (p, x)) → (iter-gk (i, x) = iter-gk (i − 1, iplus (x, ineg (q))))

Theorem: itergk i x=itergk i-1 x-q (1 < i) → (iter-gk (i, x) = iter-gk (i − 1, iplus (x, ineg (q))))

Theorem: itergk i x=itergk i-1 x-q-integer ilessp (1, i) → (iter-gk (i, x) = iter-gk (iplus (-1, i), iplus (x, ineg (q))))

Theorem: one-one+y=y integerp (y) → (iplus (1, iplus (-1, y)) = y)

Theorem: itergk i x=itergk i-j x-jq (ilessp (0, j ) ∧ ilessp (j , i)) → (iter-gk (i, x)

= iter-gk (iplus (i, ineg (j )), iplus (x, ineg (itimes (j , q)))))

Theorem: itergk i x=gk x- i-1 q-when-i>1 ilessp (1, i) → (iter-gk (i, x) = gk (iplus (x, ineg (itimes (iplus (-1, i), q)))))

Theorem: x=1-or-x>1-when-x>0 ilessp (0, x) → ((x = 1) ∨ ilessp (1, x))

Theorem: itergk i x=gk x- i-1 q ilessp (0, i) → (iter-gk (i, x) = gk (iplus (x, ineg (itimes (iplus (-1, i), q)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Introduce new constants (ie., functions with no arguments)
;  A, B, C, and E with the indicated constaints.

Conservative Axiom: a-b-c-d-intro integerp (a) ∧ integerp (b) ∧ integerp (c) ∧ integerp (d) ∧ ilessp (0, b) ∧ ilessp (0, c) ∧ ilessp (0, d)

Simultaneously, we introduce the new function symbols a, b, c, and d.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Define two functions K and K1 which will be shown to satisfy
; the generalized 91 recursion scheme with parameters
; ( (A),(B),(C),(D) ).
#| The following is the original version, which failed to be the
   correct lemma for the acceptance of the definition of K in Nqthm-1992.
   Following that is a new version.
(PROVE-LEMMA K-MEASURE-DECREASES-DEFN-K&K1
  (REWRITE)
  (IMPLIES
       (AND (NOT (ILESSP (A) X))
            (ILESSP 0
                    (IPLUS (D)
                           (IPLUS (INEG (ITIMES (B) (C)))
                                  (INEG (ITIMES (B) -1))))))
       (LESSP
        (K-MEASURE
                (A)
                (IPLUS (D)
                       (IPLUS (INEG (ITIMES (B) (C)))
                              (IPLUS (INEG (ITIMES (B) -1)) X))))
        (K-MEASURE (A) X)))
  ; hint
  ( (USE (K-MEASURE-X+Y<K-MEASURE-Y
  (A (A))
  (Y X)
  (X (IPLUS (D)
    (IPLUS (INEG (ITIMES (B) (C)))
   (INEG (ITIMES (B) -1))))))) ))
|#

Theorem: k-measure-decreases-defn-k&k1 ((¬ ilessp (a, x)) ∧ ilessp (itimes (b, c), iplus (b, d))) → (k-measure (a, iplus (b, iplus (d, iplus (ineg (itimes (b, c)), x))))

< k-measure (a, x))

Definition: k (x) = if ilessp (a, x) then iplus (x, ineg (b))

elseif ilessp (0, iplus (d, ineg (itimes (b, iplus (-1, c))))) then k (iplus (x, iplus (d, ineg (itimes (b, iplus (-1, c)))))) else a endif

Definition: k1 (x) = if ilessp (a, x) then iplus (x, ineg (b))

elseif ilessp (0, iplus (d, ineg (itimes (b, iplus (-1, c))))) then k1 (iplus (x, iplus (d, ineg (itimes (b, iplus (-1, c)))))) else iplus (a, ineg (b)) endif

Definition: iter-k (i, x) = if i ≃ 0 then x

else k (iter-k (i − 1, x)) endif

Definition: iter-k1 (i, x) = if i ≃ 0 then x

else k1 (iter-k1 (i − 1, x)) endif

Theorem: x>=x ¬ ilessp (x, x)

Theorem: iterk i x=k x- i-1 b ilessp (0, i) → (iter-k (i, x) = k (iplus (x, ineg (itimes (iplus (-1, i), b)))))

Theorem: x>=x-y-when-y>0 ilessp (0, y) → (¬ ilessp (x, iplus (x, ineg (y))))

Theorem: iterk1 i x=k1 x- i-1 b ilessp (0, i) → (iter-k1 (i, x) = k1 (iplus (x, ineg (itimes (iplus (-1, i), b)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; The two functions K and K1 satisfy the generalized 91
; recursion scheme with parameters ( (A),(B),(C),(D) ):

Theorem: x>=y+z-when-x>=y&0>=z ((¬ ilessp (x, y)) ∧ (¬ ilessp (0, z))) → (¬ ilessp (x, iplus (y, z)))

Theorem: gk x+r=s-when-p>=x&0>=r ((¬ ilessp (p, x)) ∧ (¬ ilessp (0, r))) → (gk (iplus (x, r)) = s)

Theorem: k x+d- c-1 b=a-when-a>=x&0>=d- c-1 b ((¬ ilessp (a, x)) ∧ (¬ ilessp (0, iplus (d, ineg (itimes (b, iplus (-1, c))))))) → (k (iplus (x, iplus (d, ineg (itimes (b, iplus (-1, c)))))) = a)

Theorem: k1 x+d- c-1 b=a-b-when-a>=x&0>=d- c-1 b ((¬ ilessp (a, x)) ∧ (¬ ilessp (0, iplus (d, ineg (itimes (b, iplus (-1, c))))))) → (k1 (iplus (x, iplus (d, ineg (itimes (b, iplus (-1, c))))))

= iplus (a, ineg (b)))

Theorem: itimes2–1 itimes (x, -1) = ineg (x)

Theorem: k-satisfies-gen-91-recursion k (x) = if ilessp (a, x) then iplus (x, ineg (b))

else iter-k (c, iplus (x, d)) endif

Theorem: k1-satisfies-gen-91-recursion k1 (x) = if ilessp (a, x) then iplus (x, ineg (b))

else iter-k1 (c, iplus (x, d)) endif

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; So now that it has been verified that the two functions
; K and K1 satisfy the generalized 91 recursion scheme
; with parameters ( (A),(B),(C),(D) ); we now verify that
; the two functions are not the same when
; (D) <= (B)[(C)-1].

Theorem: x-y<=0-when-x<=y (¬ ilessp (y, x)) → (¬ ilessp (0, iplus (x, ineg (y))))

Theorem: x-y<x-when-0<y ilessp (0, y) → ilessp (iplus (x, ineg (y)), x)

Theorem: k&k1-are-not-equal-functions ((¬ ilessp (itimes (b, iplus (c, -1)), d)) ∧ (¬ ilessp (a, x))) → (k (x) ≠ k1 (x))

Theorem: k&k1-are-not-equal-functions-version-2 (¬ ilessp (itimes (b, iplus (c, -1)), d)) → (k (a) ≠ k1 (a))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Introduce a new function G of one argument which
; satisfies the simpler recurrence given in Knuth's
; Theorem.

Theorem: gk-version-of-simple-recursion gk (x) = if ilessp (p, x) then iplus (x, ineg (q))

else gk (iplus (x, r)) endif

Event: Disable k-satisfies-gen-91-recursion.

Event: Disable k1-satisfies-gen-91-recursion.

Theorem: k-satisfies-simple-recursion k (x) = if ilessp (a, x) then iplus (x, ineg (b))

else k (iplus (x, iplus (d, ineg (itimes (b, iplus (-1, c)))))) endif

Conservative Axiom: g-satisfies-simple-recursion g (x) = if ilessp (a, x) then iplus (x, ineg (b))

else g (iplus (x, iplus (d, ineg (itimes (b, iplus (-1, c)))))) endif

Simultaneously, we introduce the new function symbol g.

Theorem: g=x-b-when-a<x ilessp (a, x) → (g (x) = iplus (x, ineg (b)))

Event: Disable g-satisfies-simple-recursion.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Verify that any function, such as G, which satisfies the
; simpler recurrence given in Knuth's Theorem, is in fact
; equal to K, provided (B)[(C) - 1] < (D):

Theorem: x-y>0-when-y<x ilessp (y, x) → ilessp (0, iplus (x, ineg (y)))

Theorem: lessp-k-measure (ilessp (iplus (ineg (b), itimes (b, c)), d) ∧ (¬ ilessp (a, x))) → (k-measure (a, iplus (b, iplus (d, iplus (ineg (itimes (b, c)), x))))

< k-measure (a, x))

Definition: k-induct-hint (x) = if ¬ ilessp (itimes (b, iplus (c, -1)), d) then t

elseif ilessp (a, x) then t else k-induct-hint (iplus (x,

iplus (d, ineg (itimes (b, iplus (c, -1)))))) endif

Theorem: g=k-when-b c-1 <d-induction-step (ilessp (itimes (b, iplus (c, -1)), d) ∧ (¬ ilessp (a, x)) ∧ (g (iplus (x, iplus (d, ineg (itimes (b, iplus (c, -1))))))

= k (iplus (x, iplus (d, ineg (itimes (b, iplus (c, -1)))))))) → (g (x) = k (x))

Theorem: g=k-when-b c-1 <d ilessp (itimes (b, iplus (c, -1)), d) → (g (x) = k (x))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Introduce a new function H of one argument which
; satisfies the general 91 recursion with parameters
; ( (A),(B),(C),(D) ).

Conservative Axiom: h-satisfies-gen-91-recursion (h (x) = if ilessp (a, x) then iplus (x, ineg (b))

else iter-h (c, iplus (x, d)) endif) ∧ (iter-h (i, x)

= if i ≃ 0 then x else h (iter-h (i − 1, x)) endif)

Simultaneously, we introduce the new function symbols h and iter-h.

Theorem: h=x-b-when-a<x ilessp (a, x) → (h (x) = iplus (x, ineg (b)))

Theorem: h=iterh-when-a>=x (¬ ilessp (a, x)) → (h (x) = iter-h (c, iplus (d, x)))

Theorem: iterh=x-when-i-is-zerop (i ≃ 0) → (iter-h (i, x) = x)

Event: Disable h-satisfies-gen-91-recursion.

Theorem: iterh=h-iter-h-when-not-zerop-i (i ≄ 0) → (iter-h (i, x) = h (iter-h (i − 1, x)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; To prevent looping at least one of the following
; should be disabled:

Event: Disable h=iterh-when-a>=x.

Event: Disable iterh=h-iter-h-when-not-zerop-i.

Theorem: iter-h=h iter-h (1, x) = h (x)

Theorem: iter-h-sum iter-h (i, iter-h (j , x)) = iter-h (i + j , x)

Theorem: iter-h-sum-integer (ilessp (0, i) ∧ ilessp (0, j )) → (iter-h (i, iter-h (j , x)) = iter-h (iplus (i, j ), x))

Theorem: h-satisfies-simple-rec-when-c=1 (c = 1) → (h (x)

= if ilessp (a, x) then iplus (x, ineg (b)) else h (iplus (x, iplus (d, ineg (itimes (b, iplus (c, -1)))))) endif)

Theorem: i-is-integer-when-1<i ilessp (1, i) → integerp (i)

Theorem: iterh i x=iterh i-1 x-b-when-x>a (ilessp (1, i) ∧ ilessp (a, x)) → (iter-h (i, x) = iter-h (iplus (-1, i), iplus (x, ineg (b))))

Theorem: a>=x-when-a+d>=d+x (¬ ilessp (iplus (a, d), iplus (d, x))) → (¬ ilessp (a, x))

Theorem: iterh 1+x y=iterh x h y ilessp (0, x) → (iter-h (iplus (1, x), y) = iter-h (x, h (y)))

Theorem: iterh x h y=iterh x+c-1 x+d-when-x>0&a>=y (ilessp (0, x) ∧ (¬ ilessp (a, y))) → (iter-h (x, h (y)) = iter-h (iplus (c, x), iplus (d, y)))

Theorem: iterh 1 x=iterh 1+n c-1 x+nd-induction-step-part-1 (ilessp (0, itimes (iplus (-1, n), iplus (c, -1))) ∧ (¬ ilessp (a, iplus (x, itimes (iplus (-1, n), d))))) → (iter-h (iplus (1, itimes (iplus (-1, n), iplus (c, -1))),

iplus (x, itimes (iplus (-1, n), d))) = iter-h (iplus (1, itimes (n, iplus (c, -1))), iplus (x, itimes (n, d))))

Theorem: n-1*c-1>0 (ilessp (0, n) ∧ (n ≠ 1) ∧ ilessp (1, c)) → ilessp (0, itimes (iplus (-1, n), iplus (c, -1)))

Theorem: a>=x+ n-1 d-when-a+d>=x+dn (¬ ilessp (iplus (a, d), iplus (x, itimes (d, n)))) → (¬ ilessp (a, iplus (x, itimes (iplus (-1, n), d))))

Theorem: iterh 1 x=iterh 1+n c-1 x+nd-induction-step-part-2 (ilessp (0, n) ∧ (n ≠ 1) ∧ ilessp (1, c) ∧ (¬ ilessp (iplus (a, d), iplus (x, itimes (n, d)))) ∧ (iter-h (1, x)

= iter-h (iplus (1, itimes (iplus (-1, n), iplus (c, -1))), iplus (x, itimes (iplus (-1, n), d)))))

→ (iter-h (1, x)

= iter-h (iplus (1, itimes (n, iplus (c, -1))), iplus (x, itimes (n, d))))

Theorem: a+d>=x+ n-1 d-when-a+d>=x+dn (ilessp (0, d) ∧ (¬ ilessp (iplus (a, d), iplus (x, itimes (d, n))))) → (¬ ilessp (iplus (a, d), iplus (x, itimes (iplus (-1, n), d))))

Theorem: iterh 1 x=iterh 1+n c-1 x+nd-induction-step (ilessp (0, n) ∧ (n ≠ 1) ∧ ((ilessp (1, c)

∧ ilessp (0, iplus (-1, n))

∧ (¬ ilessp (iplus (a, d), iplus (x, itimes (iplus (-1, n), d)))))

→ (iter-h (1, x)

= iter-h (iplus (1, itimes (iplus (-1, n), iplus (c, -1))), iplus (x, itimes (iplus (-1, n), d)))))

∧ ilessp (1, c) ∧ (¬ ilessp (iplus (a, d), iplus (x, itimes (n, d))))) → (iter-h (1, x)

= iter-h (iplus (1, itimes (n, iplus (c, -1))), iplus (x, itimes (n, d))))

Theorem: iterh 1 x=iterh 1+n c-1 x+nd-base-step (ilessp (1, c) ∧ (¬ ilessp (iplus (a, d), iplus (d, x)))) → (iter-h (1, x) = iter-h (c, iplus (d, x)))

Theorem: iterh 1 x=iterh 1+n c-1 x+nd (ilessp (1, c) ∧ ilessp (0, n) ∧ (¬ ilessp (iplus (a, d), iplus (x, itimes (n, d))))) → (iter-h (1, x)

= iter-h (iplus (1, itimes (n, iplus (c, -1))), iplus (x, itimes (n, d))))

Theorem: iterh i x=iterh i+n c-1 x+nd-step-1 ilessp (1, i) → (iter-h (i, x) = iter-h (iplus (-1, i), iter-h (1, x)))

Theorem: iterh i x=iterh i+n c-1 x+nd-step-2 (ilessp (1, c) ∧ ilessp (0, n) ∧ (¬ ilessp (iplus (a, d), iplus (x, itimes (n, d))))) → (iter-h (iplus (-1, i), iter-h (1, x))

= iter-h (iplus (-1, i),

iter-h (iplus (1, itimes (n, iplus (c, -1))), iplus (x, itimes (n, d)))))

Theorem: cn-n>=0-when-1<c&0<n (ilessp (1, c) ∧ ilessp (0, n)) → (¬ ilessp (iplus (ineg (n), itimes (c, n)), 0))

Theorem: iterh i x=iterh i+n c-1 x+nd-step-3 (ilessp (1, i) ∧ ilessp (1, c) ∧ ilessp (0, n)) → (iter-h (iplus (-1, i),

iter-h (iplus (1, itimes (n, iplus (c, -1))), iplus (x, itimes (n, d)))) = iter-h (iplus (i, itimes (n, iplus (c, -1))), iplus (x, itimes (n, d))))

Theorem: iterh i x=iterh i+n c-1 x+nd (ilessp (1, i) ∧ ilessp (1, c) ∧ ilessp (0, n) ∧ (¬ ilessp (iplus (a, d), iplus (x, itimes (n, d))))) → (iter-h (i, x)

= iter-h (iplus (i, itimes (n, iplus (c, -1))), iplus (x, itimes (n, d))))

Theorem: iterh i x=iterh i-1+n c-1 x+nd-b-step-1 (ilessp (1, i) ∧ ilessp (1, c) ∧ (¬ ilessp (a, x))) → (iter-h (i, x)

= iter-h (iplus (i, itimes (n (a, d, x), iplus (c, -1))), iplus (x, itimes (n (a, d, x), d))))

Theorem: i+n c-1 -1>0 (ilessp (1, i) ∧ ilessp (1, c) ∧ ilessp (0, n)) → ilessp (0, iplus (-1, iplus (i, itimes (n, iplus (c, -1)))))

Theorem: iterh i x=iterh i-1+n c-1 x+nd-b-step-2 (ilessp (1, i) ∧ ilessp (1, c) ∧ (¬ ilessp (a, x))) → (iter-h (iplus (i, itimes (n (a, d, x), iplus (c, -1))),

iplus (x, itimes (n (a, d, x), d))) = iter-h (iplus (-1, iplus (i, itimes (n (a, d, x), iplus (c, -1)))), h (iplus (x, itimes (n (a, d, x), d)))))

Theorem: iterh i x=iterh i-1+n c-1 x+nd-b-step-3 (ilessp (1, i) ∧ ilessp (1, c) ∧ (¬ ilessp (a, x))) → (iter-h (iplus (-1, iplus (i, itimes (n (a, d, x), iplus (c, -1)))),

h (iplus (x, itimes (n (a, d, x), d)))) = iter-h (iplus (-1, iplus (i, itimes (n (a, d, x), iplus (c, -1)))),

iplus (ineg (b), iplus (x, itimes (n (a, d, x), d)))))

Theorem: iterh i x=iterh i-1+n c-1 x+nd-b (ilessp (1, i) ∧ ilessp (1, c) ∧ (¬ ilessp (a, x))) → (iter-h (i, x)

= iter-h (iplus (-1, iplus (i, itimes (n (a, d, x), iplus (c, -1)))), iplus (ineg (b), iplus (x, itimes (n (a, d, x), d)))))

Theorem: x>=y-z-when-x>=y&0<z ((¬ ilessp (x, y)) ∧ ilessp (0, z)) → (¬ ilessp (x, iplus (y, ineg (z))))

Theorem: x+2-1=1+x iplus (-1, iplus (2, x)) = iplus (1, x)

Theorem: iterh i-1 x-b=iterh i-1+n c-1 x+nd-b-when-i=2 ((i = 2) ∧ ilessp (1, i) ∧ ilessp (1, c) ∧ (¬ ilessp (a, x))) → (iter-h (iplus (-1, i), iplus (x, ineg (b)))

= iter-h (iplus (-1, iplus (i, itimes (n (a, d, x), iplus (c, -1)))), iplus (ineg (b), iplus (x, itimes (n (a, d, x), d)))))

Theorem: i-1>1-when-i<>2&1<i ((i ≠ 2) ∧ ilessp (1, i)) → ilessp (1, iplus (-1, i))

Theorem: iterh i-1 x-b=iterh i-1+n c-1 x+nd-b-when-i>2 ((i ≠ 2) ∧ ilessp (1, i) ∧ ilessp (1, c) ∧ (¬ ilessp (a, x))) → (iter-h (iplus (-1, i), iplus (x, ineg (b)))

= iter-h (iplus (-1, iplus (i, itimes (n (a, d, x), iplus (c, -1)))), iplus (ineg (b), iplus (x, itimes (n (a, d, x), d)))))

Theorem: iterh i-1 x-b=iterh i-1+n c-1 x+nd-b (ilessp (1, i) ∧ ilessp (1, c) ∧ (¬ ilessp (a, x))) → (iter-h (iplus (-1, i), iplus (x, ineg (b)))

= iter-h (iplus (-1, iplus (i, itimes (n (a, d, x), iplus (c, -1)))), iplus (ineg (b), iplus (x, itimes (n (a, d, x), d)))))

Theorem: iterh i x=iterh i-1 i-b-when-a>=x (ilessp (1, i) ∧ ilessp (1, c) ∧ (¬ ilessp (a, x))) → (iter-h (i, x) = iter-h (iplus (-1, i), iplus (x, ineg (b))))

Theorem: iterh i x=iterh i-1 i-b (ilessp (1, i) ∧ ilessp (1, c)) → (iter-h (i, x) = iter-h (iplus (-1, i), iplus (x, ineg (b))))

Theorem: x*1=x-when-0<x ilessp (0, x) → (itimes (x, 1) = x)

Theorem: iterh i x=iterh i-j i-jb (ilessp (1, i) ∧ ilessp (1, c) ∧ ilessp (0, j ) ∧ ilessp (j , i)) → (iter-h (i, x) = iter-h (iplus (i, ineg (j )), iplus (x, ineg (itimes (b, j )))))

Theorem: c-1>0-when-c>1 ilessp (1, c) → ilessp (0, iplus (c, -1))

Theorem: c-1<c ilessp (iplus (c, -1), c)

Theorem: iterh c x=h x- c-1 b ilessp (1, c) → (iter-h (c, x) = h (iplus (x, ineg (itimes (b, iplus (c, -1))))))

Theorem: h x=h x+d- c-1 b (ilessp (1, c) ∧ (¬ ilessp (a, x))) → (h (x) = h (iplus (x, iplus (d, ineg (itimes (b, iplus (c, -1)))))))

Theorem: h-satisfies-simple-rec-when-c>1 ilessp (1, c) → (h (x)

= if ilessp (a, x) then iplus (x, ineg (b)) else h (iplus (x, iplus (d, ineg (itimes (b, iplus (c, -1)))))) endif)

Theorem: h-satisfies-simple-rec h (x) = if ilessp (a, x) then iplus (x, ineg (b))

else h (iplus (x, iplus (d, ineg (itimes (b, iplus (c, -1)))))) endif

Theorem: h=k-when-b c-1 <d ilessp (itimes (b, iplus (c, -1)), d) → (h (x) = k (x))

;;;;;;;;;;MAKE-LIB IS HERE;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;I am here;;;;;;;;;;;;
; (MAKE-LIB "knuth-91a")
; (MAKE-LIB-CONDITIONAL "knuth-91a" T T)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Index

a, 7–16 a<x+nd, 5 a>=x+ n-1 d-when-a+d>=x+d

n, 13 a>=x-when-a+d>=d+x, 12 a+d>=x+ n-1 d-when-a+d>=x

+dn, 13 a+d>=x+nd-when-d>0&a>=x, 5 a-b-c-d-intro, 7

b, 7–12, 15, 16

c, 7–16 c-1<c, 16 c-1>0-when-c>1, 16 cn-n>=0-when-1<c&0<n, 14 count x-1<count x, 3

d, 7–16

fn, 2 fn-intro, 2

g, 10, 11 g-satisfies-simple-recursion, 10 g=k-when-b c-1 <d, 11 g=k-when-b c-1 <d-induction

-step, 11 g=x-b-when-a<x, 10 gk, 3, 5, 6, 9, 10 gk-version-of-simple-recursion, 10 gk x+r=s-when-p>=x&0>=r, 9

h, 11, 12, 15, 16 h-satisfies-gen-91-recursion, 11 h-satisfies-simple-rec, 16 h-satisfies-simple-rec-when-c>

1, 16 h-satisfies-simple-rec-when-c=1, 12 h=iterh-when-a>=x, 11 h=k-when-b c-1 <d, 16 h=x-b-when-a<x, 11 h x=h x+d- c-1 b, 16

i+n c-1 -1>0, 14

i-1>1-when-i<>2&1<i, 15 i-is-integer-when-1<i, 12 ilessp, 2–16 induct-hint-pos-int, 4 ineg, 3–6, 8–12, 14–16 integerp, 2, 6, 7, 12 iplus, 2–6, 8–16 iter-fn, 2 iter-fn-sum, 2 iter-fn-sum-integer, 2 iter-fn=fn, 2 iter-gk, 3–6 iter-gk=gk, 3 iter-h, 11–16 iter-h-sum, 12 iter-h-sum-integer, 12 iter-h=h, 12 iter-k, 8, 9 iter-k1, 8, 9 itergk-x=itergk-x+nr, 4 itergk-x=itergk-x+nr-induction-

step, 4 itergk-x=itergk-x+r, 3 itergk=s-when-p>=x&0>=r&0

<i, 6 itergk i-1 x-q=itergk i-1 x

-q+nr, 5 itergk i x=gk x- i-1 q, 6 itergk i x=gk x- i-1 q-whe

n-i>1, 6 itergk i x=itergk i-1 x-q, 6 itergk i x=itergk i-1 x-q+n

r, 5

r-step-1, 5 r-step-2, 5 r-step-3, 5

itergk i x=itergk i-1 x-q-i nteger, 6 itergk i x=itergk i-1 x-q-w

hen-p<x, 6 hen-p>=x&0>=r, 6 hen-p>=x&r>0, 6

itergk i x=itergk i-j x-jq, 6 iterh=h-iter-h-when-not-zerop-i, 12 iterh=x-when-i-is-zerop, 11 iterh 1+x y=iterh x h y, 12 iterh 1 x=iterh 1+n c-1 x+

nd, 14 nd-base-step, 13 nd-induction-step, 13 nd-induction-step-part-1, 13 nd-induction-step-part-2, 13

iterh c x=h x- c-1 b, 16 iterh i-1 x-b=iterh i-1+n c

-1 x+nd-b, 15 -1 x+nd-b-when-i>2, 15 -1 x+nd-b-when-i=2, 15

iterh i x=iterh i+n c-1 x+ nd, 14 nd-step-1, 14 nd-step-2, 14 nd-step-3, 14

iterh i x=iterh i-1+n c-1 x+nd-b, 15 x+nd-b-step-1, 14 x+nd-b-step-2, 15 x+nd-b-step-3, 15

iterh i x=iterh i-1 i-b, 16 iterh i x=iterh i-1 i-b-whe

n-a>=x, 16 iterh i x=iterh i-1 x-b-whe

n-x>a, 12 iterh i x=iterh i-j i-jb, 16 iterh x h y=iterh x+c-1 x+

d-when-x>0&a>=y, 12 iterk1 i x=k1 x- i-1 b, 8 iterk i x=k x- i-1 b, 8 itimes, 4–6, 8–16 itimes2–1, 9

k, 8–11, 16 k-induct-hint, 11 k-measure, 3, 8, 11 k-measure-decreases-defn-k&k1, 8 k-measure-returns-numberp, 3 k-measure-x+y<k-measure-y, 3 k-satisfies-gen-91-recursion, 9 k-satisfies-simple-recursion, 10 k1, 8–10 k1-satisfies-gen-91-recursion, 9 k1 x+d- c-1 b=a-b-when-a>=

x&0>=d- c-1 b, 9 k&k1-are-not-equal-functions, 9 k&k1-are-not-equal-functions-ve

rsion-2, 10 k x+d- c-1 b=a-when-a>=x&

0>=d- c-1 b, 9

lessp-k-measure, 11

n, 5, 14, 15 n>0-when-d>o&x<=a, 5 n>=0, 5 n-1>0-when-n>0&n<>1, 4 n-1*c-1>0, 13

one-one+y=y, 6

p, 2–6, 9, 10 p+r>=x+ n-1 r-when-p+r>=x

+nr, 4 p-q-r-s-intro, 2

q, 2, 3, 5, 6, 10

r, 2–6, 9, 10

s, 2, 3, 6, 9

x<=z-when-x<y&y<=z, 4 x>=x, 8 x>=x+-y-when-y>=0, 6 x>=x-y-when-y>0, 8 x>=y+z-when-x>=y&0>=z, 9 x>=y-z-when-x>=y&0<z, 15 x>=y-z-when-x+z>=y, 4 x>=z-when-x>=y&y>=z, 5 x*1=x-when-0<x, 16 x+2-1=1+x, 15 x+ n-1 r<x+nr-when-0<r, 4 x+y>=x+-z+y-when-z>=0, 5 x-y<=0-when-x<=y, 9 x-y<x-when-0<y, 9 x-y>0-when-y<x, 10 x=1-or-x>1-when-x>0, 6