;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; 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 ).
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; The first problem to solve is: How can Knuth's problem be stated so
; the theorem prover can work on it?

; Define two mutually recursive ( partial ) functions:
;   K( a,b,c,d,x ) <== if  x > a  then  x - b
;                                 else  IterateK( a,b,c,d,c,x+d ).
;   IterateK( a,b,c,d,e,x ) <== if  e <= 1
;                                   then  K( a,b,c,d,x )
;                                   else  K( a,b,c,d,
;                                            IterateK( a,b,c,d,e-1,x))
; Knuth's parameters a, b, c, and d are included in the formal
; parameters of both K and IterateK because the theorem prover does
; not allow functions with definitions which contain "global"
; variables.
; Intuitively, IterateK iterates K e times, that is, K is applied e
; times.
; When the specified number, e, of times K is be iterated is is not
; positive, K is iterated one time.  That is, when e<1 the result in
; IterateK is the same as if e were 1.
; Thus K( a,b,c,d,x ) = IterateK( a,b,c,d,1,x ).
; Since the theorem prover does not deal with reals, the parameters
; a,b,c, and d are assumed to be integers.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; To avoid the complications of dealing with mutually recursive
; partial functions, a suggestion of M. Kaufmann is followed:
; In the definition of IterateK, replace occurrences of K with the
; body of K.
; Define a recursive partial function by
;  IterK( a,b,c,d,e,x ) <== if  1 < e
;                               then  IterK( a,b,c,d,1,
;                                            IterK( a,b,c,d,e-1,x ))
;                               else if  a < x
;                                        then  x - b
;                                        else  IterK( a,b,c,d,c,x+d).

; Then the partial function K can be defined by
;   K( a,b,c,d,x ) <== IterK( a,b,c,d,1,x ).
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; K( a,b,c,d,x ) is said to exist just in case the tuple of integers
; ( a,b,c,d,x ) is in the domain of those input values where the
; partial function K halts and produces output values.
; Knuth's theorem follows from parts 1, 4, 6, 8, and 9 of the
; following Main Theorem.
;  1. If  x > a, then  K( a,b,c,d,x )  exists.
;  2. If  x <= a, d <= 0, and c <= 1, then  K( a,b,c,d,x )  does not
;     exist.
;  3. If  x <= a, d <= 0, and c > 1, then  K( a,b,c,d,x )  does not
;     exist.
;  4. If  x <= a, d > 0, and c <= 1, then  K( a,b,c,d,x )  exists.
;  5. If  x <= a, d > 0, c > 1, and b <= 0, then  K( a,b,c,d,x )
;     exists.
;  6. If  x <= a, d > 0, c > 1, and b > 0, then  K( a,b,c,d,x )
;     exists if and only if  K( a,b,c,d,x+d-(c-1)b )  exists and
;     K( a,b,c,d,x ) = K( a,b,c,d,x+d-(c-1)b ).
;  7. If  d > 0, c > 1, b > 0, and (c-1)b < d, then
;     K( a,b,c,d,x )  exists if and only if  K( a,b,1,d-(c-1)b,x )
;     exists and  K( a,b,c,d,x ) = K( a,b,1,d-(c-1)b,x ).
;  8. If  d > 0, c > 1, b > 0, and (c-1)b < d, then
;     K( a,b,c,d,x ) exists.
;  9. If  x <= a, d > 0, c > 1, b > 0, and (c-1)b >= d, then
;     K( a,b,c,d,x ) does not exist
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Use the library of integer facts.

Event: Start with the library "integers".

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Define the partial function IterK using EVAL$,
; and define the partial function K using IterK.

Definition: iterk (a, b, c, d, e, x) = eval$ (t,

         '(if
           (ilessp '1 e)
           (iterk a b c d
            '1
            (iterk a b c d (idifference e '1) x))
           (if
            (ilessp a x)
            (idifference x b)
            (iterk a b c d c (iplus x d)))),

list (cons ('a, a), cons ('b, b), cons ('c, c), cons ('d, d), cons ('e, e), cons ('x, x)))

Definition: k (a, b, c, d, x) = iterk (a, b, c, d, 1, x)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Recursively distribute V&C-APPLY$ throughout the body of the
; defintion of ITERK. Break the definition into several cases.

Theorem: iterk-exists-iff-body-exists v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0)))

↔ v&c-apply$ ('if,

list (v&c-apply$ ('ilessp, list ('(1 . 0), cons (e, 0))),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

v&c-apply$ ('idifference,

cons (cons (e,

0),

               '((1
                  . 0)))),

cons (x, 0))))),

v&c-apply$ ('if,

list (v&c-apply$ ('ilessp,

list (cons (a, 0), cons (x, 0))),

v&c-apply$ ('idifference,

list (cons (x, 0), cons (b, 0))),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (c, 0), v&c-apply$ ('iplus,

list (cons (x,

0), cons (d,

0)))))))))

Theorem: iterk-value=body-value car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0))))

= car (v&c-apply$ ('if,

list (v&c-apply$ ('ilessp, list ('(1 . 0), cons (e, 0))),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

v&c-apply$ ('idifference,

cons (cons (e,

0),

               '((1
                  . 0)))),

cons (x, 0))))),

v&c-apply$ ('if,

list (v&c-apply$ ('ilessp,

list (cons (a, 0),

cons (x, 0))),

v&c-apply$ ('idifference,

list (cons (x, 0),

cons (b, 0))),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (c, 0), v&c-apply$ ('iplus,

list (cons (x,

0), cons (d,

0))))))))))

Theorem: cost-is-a-numberp cdr (v&c-apply$ (fn, args)) ∈ N

Theorem: cost>0-if-fn-exists v&c-apply$ (fn, args) → (0 < cdr (v&c-apply$ (fn, args)))

Theorem: iterk-cost>body-cost v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0)))

→ (cdr (v&c-apply$ ('if,

list (v&c-apply$ ('ilessp, list ('(1 . 0), cons (e, 0))),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

v&c-apply$ ('idifference,

cons (cons (e,

0),

               '((1
                  . 0)))),

cons (x, 0))))),

v&c-apply$ ('if,

list (v&c-apply$ ('ilessp,

list (cons (a, 0),

cons (x, 0))),

v&c-apply$ ('idifference,

list (cons (x, 0),

cons (b, 0))),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (c, 0), v&c-apply$ ('iplus,

list (cons (x,

0), cons (d,

0))))))))))

< cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0)))))

Theorem: v&c-apply$-if v&c-apply$ ('if, args) = if car (args)

then if caar (args) then fix-cost (cadr (args), 1 + cdar (args)) else fix-cost (caddr (args), 1 + cdar (args)) endif

else f endif

Theorem: iterk-exists-iff-body-exists-when-e>1 ilessp (1, e) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0)))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                       '(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                                     v&c-apply$ ('idifference,

cons (cons (e, 0),

                                                    '((1 . 0)))),

cons (x, 0))))))

Theorem: iterk-value=body-value-when-e>1 ilessp (1, e) → (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0))))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

    '(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                  v&c-apply$ ('idifference,

cons (cons (e, 0),

                                 '((1
                                    . 0)))),

cons (x, 0)))))))

Theorem: iterk-cost>body-cost-when-e>1 (ilessp (1, e) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0))))

→ (cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

              v&c-apply$ ('idifference,

cons (cons (e, 0),

                              '((1 . 0)))),

cons (x, 0))))))

< cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0)))))

Theorem: eq-args-give-eq-existence

((fn ≠ 'quote)

∧ (fn ≠ 'if) ∧ (strip-cars (args1 ) = strip-cars (args2 )) ∧ ((f ∈ args1 ) = (f ∈ args2 ))) → (v&c-apply$ (fn, args1 ) ↔ v&c-apply$ (fn, args2 ))

Theorem: eq-args-give-eq-values

((fn ≠ 'quote)

∧ (fn ≠ 'if) ∧ (strip-cars (args1 ) = strip-cars (args2 )) ∧ ((f ∈ args1 ) = (f ∈ args2 ))) → (car (v&c-apply$ (fn, args1 )) = car (v&c-apply$ (fn, args2 )))

Theorem: eq-args-cost-depends-on-cost-of-args ((fn ≠ 'if) ∧ (sum-cdrs (args1 ) < sum-cdrs (args2 )) ∧ (strip-cars (args1 ) = strip-cars (args2 )) ∧ v&c-apply$ (fn, args1 ) ∧ v&c-apply$ (fn, args2 )) → (cdr (v&c-apply$ (fn, args1 )) < cdr (v&c-apply$ (fn, args2 )))

Theorem: iterk-v&c-apply$-idifference-exists v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), v&c-apply$ ('idifference, cons (cons (e, 0), '((1 . 0)))), cons (x, 0)))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (idifference (e, 1), 0), cons (x, 0)))

Theorem: iterk-v&c-apply$-idifference-value car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                  v&c-apply$ ('idifference,

cons (cons (e, 0), '((1 . 0)))),

cons (x, 0))))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (idifference (e, 1), 0), cons (x, 0))))

Theorem: iterk-v&c-apply$-idifference-cost v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (idifference (e, 1), 0), cons (x, 0)))

→ (cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (idifference (e, 1), 0), cons (x, 0))))

< cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                          v&c-apply$ ('idifference,

cons (cons (e, 0), '((1 . 0)))),

cons (x, 0)))))

Theorem: iterk-exists-iff-body-exists-when-e>1-version-2 ilessp (1, e) → (v&c-apply$ ('iterk, list (cons (a, 0),

cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0)))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

    '(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (idifference (e, 1), 0), cons (x, 0))))))

Theorem: iterk-value=body-value-when-e>1-version-2 ilessp (1, e) → (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0))))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

       '(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (idifference (e, 1), 0), cons (x, 0)))))))

Theorem: args-exist-when-fn-exists ((fn ≠ 'if) ∧ v&c-apply$ (fn, args)) → (f ∉ args)

Theorem: iterk-cost>body-cost-when-e>1-version-2 (ilessp (1, e) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0))))

→ (cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (idifference (e, 1), 0), cons (x, 0))))))

< cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0)))))

Theorem: iterk-exists-iff-body-exists-when-e>1-version-3-case-1 (vc-x ∧ ilessp (1, e)) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), vc-x))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (idifference (e, 1), 0), vc-x)))))

Theorem: iterk-exists-iff-body-exists-when-e>1-version-3-case-2 ((vc-x = f) ∧ ilessp (1, e)) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), vc-x))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (idifference (e, 1), 0), vc-x)))))

Theorem: iterk-exists-iff-body-exists-when-e>1-version-3 ilessp (1, e) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), vc-x))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (idifference (e, 1), 0), vc-x)))))

Theorem: iterk-value=body-value-when-e>1-version-3-case-1 (vc-x ∧ ilessp (1, e)) → (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), vc-x)))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

    '(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (idifference (e, 1), 0), vc-x))))))

Theorem: iterk-value=body-value-when-e>1-version-3-case-2 ((vc-x = f) ∧ ilessp (1, e)) → (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), vc-x)))

= car (v&c-apply$ ('iterk, list (cons (a, 0),

cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (idifference (e, 1), 0), vc-x))))))

Theorem: iterk-value=body-value-when-e>1-version-3 ilessp (1, e) → (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), vc-x)))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (idifference (e, 1), 0), vc-x))))))

Theorem: iterk-exists-when-e<=1&a<x ((¬ ilessp (1, e)) ∧ ilessp (a, x)) → v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0)))

Theorem: iterk-value-when-e<=1&a<x ((¬ ilessp (1, e)) ∧ ilessp (a, x)) → (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0))))

= idifference (x, b))

Theorem: iterk-exists-iff-body-exists-when-e<=1&a>=x ((¬ ilessp (1, e)) ∧ (¬ ilessp (a, x))) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0)))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (c, 0), v&c-apply$ ('iplus,

list (cons (x, 0), cons (d, 0))))))

Theorem: iterk-value=body-value-when-e<=1&a>=x ((¬ ilessp (1, e)) ∧ (¬ ilessp (a, x))) → (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0))))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (c, 0), v&c-apply$ ('iplus,

list (cons (x, 0), cons (d, 0)))))))

Theorem: iterk-cost>body-cost-when-e<=1&a>=x ((¬ ilessp (1, e)) ∧ (¬ ilessp (a, x)) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0))))

→ (cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (c, 0), v&c-apply$ ('iplus, list (cons (x, 0), cons (d, 0))))))

< cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0)))))

Event: Disable iterk-exists-iff-body-exists.

Event: Disable iterk-value=body-value.

Event: Disable iterk-cost>body-cost.

Theorem: iterk-exists-iff-body-exists-when-e<=1&a>=x-version-2 ((¬ ilessp (1, e)) ∧ (¬ ilessp (a, x))) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0)))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (c, 0), cons (iplus (x, d), 0))))

Theorem: iterk-value=body-value-when-e<=1&a>=x-version-2 ((¬ ilessp (1, e)) ∧ (¬ ilessp (a, x))) → (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0))))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (c, 0), cons (iplus (x, d), 0)))))

Theorem: iterk-cost>body-cost-when-e<=1&a>=x-version-2 ((¬ ilessp (1, e)) ∧ (¬ ilessp (a, x)) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0))))

→ (cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (c, 0), cons (iplus (x, d), 0))))

< cdr (v&c-apply$ ('iterk, list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0)))))

Event: Disable iterk-exists-iff-body-exists-when-e>1.

Event: Disable iterk-value=body-value-when-e>1.

Event: Disable iterk-cost>body-cost-when-e>1.

Event: Disable iterk-exists-iff-body-exists-when-e<=1&a>=x.

Event: Disable iterk-value=body-value-when-e<=1&a>=x.

Event: Disable iterk-cost>body-cost-when-e<=1&a>=x.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; The next two events are versions of Part 1 of the
; Main Theorem given above in the introduction.
;  1. If  x > a, then  K( a,b,c,d,x )  exists.
;     Proof.  By the definitions of IterK and K.

Theorem: k-exists-when-x>a ilessp (a, x) → v&c-apply$ ('k,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (x, 0)))

Theorem: k-halts-when-x>a (vc-a ∧ vc-b ∧ vc-c ∧ vc-d ∧ vc-x ∧ ilessp (car (vc-a), car (vc-x))) → v&c-apply$ ('k, list (vc-a, vc-b, vc-c, vc-d, vc-x))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Lemma 1. The cost of computing IterK is unbounded
;          when x <= a, d <= 0, and c <= 1:
;  Assume  x <= a, d <= 0, c <= 1, i > 0,
;   and

;  IterK( a,b,c,d,1,x ) exists.
;  Then IterK( a,b,c,d,c,x+id ) exists
;   and
;  cost[ IterK( a,b,c,d,c,x+id ) ] + i-1
;   <
;  cost[ IterK( a,b,c,d,1,x ) ].
; Proof. By induction on i.

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

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

elseif x = 1 then t

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

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

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

Theorem: iterk x+ i-1 d implies iterk x+id-when-x<=a&d<=0&c<=1&i>0 ((¬ ilessp (a, x)) ∧ (¬ ilessp (0, d)) ∧ (¬ ilessp (1, c)) ∧ ilessp (0, i) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (c, 0), cons (iplus (x, itimes (iplus (-1, i), d)), 0))))

→ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (c, 0), cons (iplus (x, itimes (d, i)), 0)))

Theorem: iterk-e=1&x-implies-iterk-e=c&x+id-when-x<=a&d<=0&c<=1 ((¬ ilessp (a, x)) ∧ (¬ ilessp (0, d)) ∧ (¬ ilessp (1, c)) ∧ ilessp (0, i) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (1, 0), cons (x, 0))))

→ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (c, 0), cons (iplus (x, itimes (i, d)), 0)))

Theorem: w-1+y<z&x<y-implies-w+x<z (ilessp (0, w) ∧ (x < y) ∧ ((iplus (-1, w) + y) < z)) → (((w + x) < z) = t)

Theorem: cost-induction-step-when-x<=a&d<=0&c<=1 ((¬ ilessp (a, x)) ∧ (¬ ilessp (0, d)) ∧ (¬ ilessp (1, c)) ∧ ilessp (0, i) ∧ (i ≠ 1) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                  '(1 . 0),

cons (x, 0)))

∧ ((cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (c, 0), cons (iplus (x, itimes (iplus (-1, i), d)), 0))))

+ iplus (-1, iplus (-1, i))) < cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

    '(1 . 0),

cons (x, 0))))))

→ ((cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (c, 0), cons (iplus (x, itimes (d, i)), 0))))

+ iplus (-1, i)) < cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

    '(1 . 0),

cons (x, 0)))))

Theorem: cost-base-step-when-x<=a&d<=0&c<=1 ((¬ ilessp (a, x)) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (1, 0), cons (x, 0))))

→ (cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (c, 0), cons (iplus (d, x), 0))))

< cdr (v&c-apply$ ('iterk, list (cons (a, 0),

cons (b, 0), cons (c, 0), cons (d, 0), cons (1, 0), cons (x, 0)))))

Theorem: iterk-e=1&x-cost>i-1+cost-iterk-e=c&x+id-when-x<=a&d<=0&c<=1 ((¬ ilessp (a, x)) ∧ (¬ ilessp (0, d)) ∧ (¬ ilessp (1, c)) ∧ ilessp (0, i) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

cons (x, 0))))

→ ((cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (c, 0), cons (iplus (x, itimes (i, d)), 0))))

+ iplus (-1, i)) < cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

cons (x, 0)))))

Theorem: y<=z-when-x+y-1<z&x>=0&y>0 ((x ∈ N) ∧ ilessp (0, y) ∧ ((x + iplus (-1, y)) < z)) → ((z ≮ y) = t)

Theorem: iterk-cost-is-unbounded-when-x<=a&d<=0&c<=1 ((¬ ilessp (a, x)) ∧ (¬ ilessp (0, d)) ∧ (¬ ilessp (1, c)) ∧ ilessp (0, i) ∧ v&c-apply$ ('iterk, list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                   '(1 . 0),

cons (x, 0))))

→ (cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                       '(1 . 0),

cons (x, 0))))

≮ i)

Theorem: ilessp-0-add1-x ilessp (0, 1 + x)

Theorem: iterk-does-not-exist-when-x<=a&d<=0&c<=1 ((¬ ilessp (a, x)) ∧ (¬ ilessp (0, d)) ∧ (¬ ilessp (1, c))) → (¬ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                     '(1 . 0),

cons (x, 0))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; The next two events are versions of Part 2 of the
; Main Theorem given above in the introduction.
;  2. If  x <= a, d <= 0, and c <= 1, then
;     K( a,b,c,d,x )  does not exist.
;     Proof. By Lemma 1 and the definition of K.

Theorem: k-does-not-exist-when-x<=a&d<=0&c<=1 ((¬ ilessp (a, x)) ∧ (¬ ilessp (0, d)) ∧ (¬ ilessp (1, c))) → (¬ v&c-apply$ ('k,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (x, 0))))

Theorem: k-does-not-halt-when-x<=a&d<=0&c<=1 (vc-a ∧ vc-b ∧ vc-c ∧ vc-d ∧ vc-x ∧ (¬ ilessp (car (vc-a), car (vc-x))) ∧ (¬ ilessp (0, car (vc-d))) ∧ (¬ ilessp (1, car (vc-c)))) → (¬ v&c-apply$ ('k, list (vc-a, vc-b, vc-c, vc-d, vc-x)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Lemma 2. When the number of iterates is positive,
;          the cost of computing IterK is an order
;          homomorhism of the number of iterates:
;  Assume that  0 < e1 < e2
;   and
;  IterK( a,b,c,d,e2,x ) exists.
;  Then  IterK( a,b,c,d,e1,x ) also exists
;   and
;  cost[ IterK( a,b,c,d,e1,x ) ]
;   <
;  cost[ IterK( a,b,c,d,e2,x ) ].
; Proof.  Hold e1 constant and induct on e2.

Theorem: count-sub1-y<count-y-when-0<x<y (ilessp (0, x) ∧ ilessp (x, y)) → (count (iplus (-1, y)) < count (y))

Definition: induct-hint-cost-hom (x, y) = if ¬ ilessp (0, x) then t

elseif ¬ ilessp (x, y) then t elseif x = iplus (-1, y) then t else induct-hint-cost-hom (x, iplus (-1, y)) endif

Theorem: y>1-when-y>x&x>0 (ilessp (0, x) ∧ ilessp (x, y)) → ilessp (1, y)

Theorem: iterk-at-e1-exists-when-iterk-at-e2-exists&0<e1<e2-basic-step (ilessp (0, e1 ) ∧ ilessp (e1 , e2 ) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e2 , 0), cons (x, 0))))

→ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e2 ), 0), cons (x, 0)))

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

Theorem: iterk-at-e1-exists-when-iterk-at-e2-exists&0<e1<e2 (ilessp (0, e1 ) ∧ ilessp (e1 , e2 ) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e2 , 0), cons (x, 0))))

→ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e1 , 0), cons (x, 0)))

Theorem: cost>cost-of-args ((fn ≠ 'if) ∧ (f ∉ args) ∧ v&c-apply$ (fn, args)) → (sum-cdrs (args) < cdr (v&c-apply$ (fn, args)))

Theorem: sum-cdrs>=member (x ∈ l) → (sum-cdrs (l) ≮ cdr (x))

Theorem: cost>member (v&c-apply$ (fn, args) ∧ (fn ≠ 'if) ∧ (x ∈ args)) → (cdr (x) < cdr (v&c-apply$ (fn, args)))

Theorem: cost-iterk-at-e1<cost-iterk-at-e2-when-0<e1<e2-basic-step (ilessp (0, e1 ) ∧ ilessp (e1 , e2 ) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e2 , 0), cons (x, 0))))

→ (cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e2 ), 0), cons (x, 0))))

< cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e2 , 0), cons (x, 0)))))

Event: Disable y>1-when-y>x&x>0.

Theorem: cost-iterk-at-e1<cost-iterk-at-e2-when-0<e1<e2 (ilessp (0, e1 ) ∧ ilessp (e1 , e2 ) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e2 , 0), cons (x, 0))))

→ (cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e1 , 0), cons (x, 0))))

< cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e2 , 0), cons (x, 0)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Lemma 3. The cost of computing IterK is unbounded
;          when x <= a, d <= 0, and c > 1:
;  Assume  x <= a, d <= 0, c > 1, i > 0,
;   and
;  IterK( a,b,c,d,1,x ) exists.
;  Then IterK( a,b,c,d,1,x+id ) exists
;   and
;  cost[ IterK( a,b,c,d,1,x+id ) ] + i
;   <
;  cost[ IterK( a,b,c,d,1,x ) ].
; Proof. By induction on i.

Theorem: iterk x+ i-1 d implies iterk x+id-when-x<=a&d<=0&c>1&i>0&e=1 ((¬ ilessp (a, x)) ∧ (¬ ilessp (0, d)) ∧ ilessp (1, c) ∧ ilessp (0, i) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                   '(1 . 0),

cons (iplus (x, itimes (iplus (-1, i), d)), 0))))

→ v&c-apply$ ('iterk, list (cons (a, 0),

cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

cons (iplus (x, itimes (d, i)), 0)))

Theorem: iterk-x-implies-iterk-x+id-when-x<=a&d<=0&c>1&e=1 ((¬ ilessp (a, x)) ∧ (¬ ilessp (0, d)) ∧ ilessp (1, c) ∧ ilessp (0, i) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

cons (x, 0))))

→ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

cons (iplus (x, itimes (i, d)), 0)))

Theorem: iterk-x+d-cost<cost-iterk-x-when-a>=x&1<c ((¬ ilessp (a, x)) ∧ ilessp (1, c) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

cons (x, 0))))

→ (cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

    '(1 . 0),

cons (iplus (x, d), 0))))

< cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                          '(1 . 0),

cons (x, 0)))))

Theorem: cost-induction-step-when-x<=a&d<=0&c>1 ((¬ ilessp (a, x)) ∧ (¬ ilessp (0, d)) ∧ ilessp (1, c) ∧ ilessp (0, i) ∧ (i ≠ 1) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                  '(1 . 0),

cons (x, 0)))

∧ ((cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                       '(1 . 0),

cons (iplus (x, itimes (iplus (-1, i), d)), 0))))

+ iplus (-1, i))

< cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                          '(1 . 0),

cons (x, 0))))))

→ ((cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                       '(1 . 0),

cons (iplus (x, itimes (d, i)), 0))))

+ i)

< cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

cons (x, 0)))))

Theorem: iterk-x-cost>i+cost-iterk-x+id-when-x<=a&d<=0&c>1&e=1 ((¬ ilessp (a, x)) ∧ (¬ ilessp (0, d)) ∧ ilessp (1, c) ∧ ilessp (0, i) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

cons (x, 0))))

→ ((cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

cons (iplus (x, itimes (i, d)), 0))))

+ i) < cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

cons (x, 0)))))

Theorem: iterk-cost-is-unbounded-when-x<=a&d<=0&c>1 ((¬ ilessp (a, x)) ∧ (¬ ilessp (0, d)) ∧ ilessp (1, c) ∧ ilessp (0, i) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                   '(1 . 0),

cons (x, 0))))

→ (i < cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                           '(1 . 0),

cons (x, 0)))))

Theorem: iterk-does-not-exist-when-x<=a&d<=0&c>1 ((¬ ilessp (a, x)) ∧ (¬ ilessp (0, d)) ∧ ilessp (1, c)) → (¬ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                     '(1 . 0),

cons (x, 0))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; The next two events are versions of Part 3 of the
; Main Theorem given above in the introduction.
;  3. If  x <= a, d <= 0, and c > 1, then
;     K( a,b,c,d,x )  does not exist.
;     Proof. By Lemma 3 and the definition of K.

Theorem: k-does-not-exist-when-x<=a&d<=0&c>1 ((¬ ilessp (a, x)) ∧ (¬ ilessp (0, d)) ∧ ilessp (1, c)) → (¬ v&c-apply$ ('k,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (x, 0))))

Theorem: k-does-not-halt-when-x<=a&d<=0&c>1 (vc-a ∧ vc-b ∧ vc-c ∧ vc-d ∧ vc-x ∧ (¬ ilessp (car (vc-a), car (vc-x))) ∧ (¬ ilessp (0, car (vc-d))) ∧ ilessp (1, car (vc-c))) → (¬ v&c-apply$ ('k, list (vc-a, vc-b, vc-c, vc-d, vc-x)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Lemma 4. IterK exists when d > 0,
;          c <= 1, and e = c:
;  Assume  d > 0, and c <= 1.
;  Then IterK( a,b,c,d,c,x ) exists.
; Proof. Hold the parameter a fixed and
;        induct on the value given by
;        if  x > a  then  0
;                   else  1 + a - x.

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

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

Theorem: k-measure x+d<k-measure x-when-0<d&a>=x (ilessp (0, d) ∧ (¬ ilessp (a, x))) → (k-measure (a, iplus (d, x)) < k-measure (a, x))

Event: Disable k-measure.

Definition: induct-hint-k-measure (a, b, c, d, x) = if ¬ ilessp (0, d) then t

elseif ilessp (a, x) then t

else induct-hint-k-measure (a, b, c, d, iplus (d, x)) endif

Theorem: iterk-exists-when-d>0&c<=1&e=c (ilessp (0, d) ∧ (¬ ilessp (1, c))) → v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (c, 0), cons (x, 0)))

Theorem: iterk-exists-when-x<=a&d>0&c<=1&e=1 ((¬ ilessp (a, x)) ∧ ilessp (0, d) ∧ (¬ ilessp (1, c))) → v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                   '(1 . 0),

cons (x, 0)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; The next two events are versions of Part 4 of the
; Main Theorem given above in the introduction.
;  4. If  x <= a, d > 0, and c <= 1, then
;      K( a,b,c,d,x )  exists.
;     Proof. By Lemma 4 and the definition of K.

Theorem: k-exists-when-x<=a&d>0&c<=1 ((¬ ilessp (a, x)) ∧ ilessp (0, d) ∧ (¬ ilessp (1, c))) → v&c-apply$ ('k,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (x, 0)))

Theorem: k-halts-when-x<=a&d>0&c<=1 (vc-a ∧ vc-b ∧ vc-c ∧ vc-d ∧ vc-x ∧ (¬ ilessp (car (vc-a), car (vc-x))) ∧ ilessp (0, car (vc-d)) ∧ (¬ ilessp (1, car (vc-c)))) → v&c-apply$ ('k, list (vc-a, vc-b, vc-c, vc-d, vc-x))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Lemma 5. IterK exists and has value > a
;          when x > a, b <= 0, and e > 0:

;  Assume  x > a, b <= 0, and e > 0.
;  Then IterK( a,b,c,d,e,x ) exists
;   and
;  IterK( a,b,c,d,e,x ) > a.
; Proof.  By induction on e.

Theorem: iterk-exists-when-e<=1&a<x-version-2 (vc-x ∧ (¬ ilessp (1, e)) ∧ ilessp (a, car (vc-x))) → v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), vc-x))

Theorem: iterk-value-when-e<=1&a<x-version-2 (vc-x ∧ (¬ ilessp (1, e)) ∧ ilessp (a, car (vc-x))) → (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), vc-x)))

= idifference (car (vc-x), b))

Theorem: a+b<x-when-a<x&b<=0 (ilessp (a, x) ∧ (¬ ilessp (0, b))) → ilessp (iplus (a, b), x)

Theorem: a<-b+x-when-a<x&b<=0 (ilessp (a, x) ∧ (¬ ilessp (0, b))) → ilessp (a, iplus (ineg (b), x))

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

Theorem: iterk-exists&iterk>a-when-x>a&b<=0&e>0 (ilessp (a, x) ∧ (¬ ilessp (0, b)) ∧ ilessp (0, e)) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0)))

∧ ilessp (a,

car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Lemma 6. The number of iterates in the composition
;          of IterK with itself add up:
;  Let  e1 > 0  and  e2 > 0.  Then
;  IterK( a,b,c,d,e1,IterK( a,b,c,d,e2,x ) ) exists
;   iff
;  IterK( a,b,c,d,e1+e2,x ) exists
;  and
;  IterK( a,b,c,d,e1,IterK( a,b,c,d,e2,x ) )
;   =
;  IterK( a,b,c,d,e1+e2,x )
; Proof.  By induction on e1.

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

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

Theorem: nbr-of-iterates-sum-exists-step-1 (ilessp (0, e1 ) ∧ (e1 ≠ 1)) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e1 , 0), v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e2 , 0), cons (x, 0)))))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e1 ), 0), v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e2 , 0), cons (x, 0))))))))

Theorem: nbr-of-iterates-sum-values-step-1 (ilessp (0, e1 ) ∧ (e1 ≠ 1)) → (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e1 , 0), v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e2 , 0), cons (x, 0))))))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e1 ), 0), v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e2 , 0), cons (x, 0)))))))))

Theorem: nbr-of-iterates-sum-exists-step-2 (ilessp (0, e1 ) ∧ (e1 ≠ 1) ∧ ilessp (0, e2 )) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (e1 , e2 ), 0), cons (x, 0)))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (iplus (-1, e1 ), e2 ),

0), cons (x, 0))))))

Theorem: nbr-of-iterates-sum-values-step-2 (ilessp (0, e1 ) ∧ (e1 ≠ 1) ∧ ilessp (0, e2 )) → (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (e1 , e2 ), 0), cons (x, 0))))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

    '(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (iplus (-1, e1 ), e2 ),

0), cons (x, 0)))))))

Theorem: nbr-of-iterates-sum-exists-step-3 ((v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e1 ), 0), v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e2 , 0), cons (x, 0)))))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (iplus (-1, e1 ), e2 ), 0), cons (x, 0))))

∧ (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e1 ), 0), v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e2 , 0), cons (x, 0))))))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (iplus (-1, e1 ), e2 ), 0), cons (x, 0))))))

→ (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e1 ), 0), v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e2 , 0), cons (x, 0)))))))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, iplus (e1 , e2 )),

0), cons (x, 0))))))

Theorem: nbr-of-iterates-sum-values-step-3 ((v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e1 ), 0), v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e2 , 0), cons (x, 0)))))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (iplus (-1, e1 ), e2 ), 0), cons (x, 0))))

∧ (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e1 ), 0), v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e2 , 0), cons (x, 0))))))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (iplus (-1, e1 ), e2 ), 0), cons (x, 0))))))

→ (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e1 ), 0), v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e2 , 0), cons (x, 0))))))))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

    '(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1,

iplus (e1 , e2 )), 0), cons (x, 0)))))))

Theorem: nbr-of-iterates-sum-exists&values (ilessp (0, e1 ) ∧ ilessp (0, e2 )) → ((v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e1 , 0), v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e2 , 0), cons (x, 0)))))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (e1 , e2 ), 0), cons (x, 0))))

∧ (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e1 , 0), v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e2 , 0), cons (x, 0))))))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (e1 , e2 ), 0), cons (x, 0))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Lemma 7. The number of iterates of K accumulate
;          when 1 < c, 0 < d, and x is "small."
;  Assume 1 < c, 0 < d, 0 < n, and a+d >= x+nd.
;  Then
;  IterK( a,b,c,d,1,x ) exists
;   iff
;  IterK( a,b,c,d,1+n(c-1),x+nd ) exists
;  and
;  IterK( a,b,c,d,1,x )
;   =
;  IterK( a,b,c,d,1+n(c-1),x+nd ).
; Proof.  By induction on n.

Theorem: n c-1 +1=c-when-n=1&c>1 ((n = 1) ∧ ilessp (1, c)) → (iplus (1, itimes (n, iplus (-1, c))) = c)

Theorem: nd=d-when-n=1&d>0 ((n = 1) ∧ ilessp (0, d)) → (itimes (n, d) = d)

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

Theorem: iterk e=1+ n c-1&x+nd-exists-base-step ((n = 1) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ (¬ ilessp (iplus (a, d), iplus (x, itimes (n, d))))) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                    '(1 . 0),

cons (x, 0)))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (1, itimes (n, iplus (-1, c))), 0), cons (iplus (x, itimes (n, d)), 0))))

Theorem: iterk e=1+ n c-1&x+nd-value-base-step ((n = 1) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ (¬ ilessp (iplus (a, d), iplus (x, itimes (n, d))))) → (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

cons (x, 0))))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (1, itimes (n, iplus (-1, c))), 0), cons (iplus (x, itimes (n, d)), 0)))))

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

Theorem: iterk e=1+ n c-1&x+nd-exists-step-1 (ilessp (1, c) ∧ ilessp (0, n) ∧ (n ≠ 1)) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (1, itimes (iplus (-1, n), iplus (-1, c))), 0), cons (iplus (x, itimes (iplus (-1, n), d)), 0)))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (itimes (iplus (-1, n), iplus (-1, c)), 0), v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

               '(1 . 0),

cons (iplus (x,

itimes (iplus (-1, n), d)),

0))))))

Theorem: iterk e=1+ n c-1&x+nd-value-step-1 (ilessp (1, c) ∧ ilessp (0, n) ∧ (n ≠ 1)) → (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (1, itimes (iplus (-1, n), iplus (-1, c))),

0), cons (iplus (x, itimes (iplus (-1, n), d)), 0))))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (itimes (iplus (-1, n), iplus (-1, c)), 0), v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                  '(1 . 0),

cons (iplus (x,

itimes (iplus (-1,

n), d)),

0)))))))

Theorem: iterk e=1+ n c-1&x+nd-exists-step-2 (ilessp (0, n) ∧ ilessp (0, d) ∧ (¬ ilessp (iplus (a, d), iplus (x, itimes (n, d))))) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (itimes (iplus (-1, n), iplus (-1, c)), 0), v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

cons (iplus (x, itimes (iplus (-1, n), d)),

0)))))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (itimes (iplus (-1, n), iplus (-1, c)), 0), v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (c, 0), cons (iplus (x, itimes (n, d)), 0))))))

Theorem: iterk e=1+ n c-1&x+nd-value-step-2 (ilessp (0, n) ∧ ilessp (0, d) ∧ (¬ ilessp (iplus (a, d), iplus (x, itimes (n, d))))) → (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (itimes (iplus (-1, n), iplus (-1, c)), 0), v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

    '(1 . 0),

cons (iplus (x,

itimes (iplus (-1, n), d)), 0))))))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (itimes (iplus (-1, n), iplus (-1, c)), 0), v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (c, 0), cons (iplus (x, itimes (n, d)),

0)))))))

Theorem: iterk e=1+ n c-1&x+nd-exists-step-3 (ilessp (0, n) ∧ (n ≠ 1) ∧ ilessp (1, c)) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (itimes (iplus (-1, n), iplus (-1, c)), 0), v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (c, 0), cons (iplus (x, itimes (n, d)), 0)))))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (1, itimes (n, iplus (-1, c))), 0), cons (iplus (x, itimes (n, d)), 0))))

Theorem: iterk e=1+ n c-1&x+nd-value-step-3 (ilessp (0, n) ∧ (n ≠ 1) ∧ ilessp (1, c)) → (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (itimes (iplus (-1, n), iplus (-1, c)), 0), v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (c, 0), cons (iplus (x, itimes (n, d)), 0))))))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (1, itimes (n, iplus (-1, c))), 0), cons (iplus (x, itimes (n, d)), 0)))))

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

Theorem: iterk e=1+ n c-1&x+nd-exists-when-1<c&0<d&0<n&a+d>=x+nd (ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (0, n) ∧ (¬ ilessp (iplus (a, d), iplus (x, itimes (n, d))))) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

cons (x, 0)))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (1, itimes (n, iplus (-1, c))), 0), cons (iplus (x, itimes (n, d)), 0))))

Theorem: iterk e=1+ n c-1&x+nd-value-when-1<c&0<d&0<n&a+d>=x+nd (ilessp (1, c)

∧ ilessp (0, d) ∧ ilessp (0, n) ∧ (¬ ilessp (iplus (a, d), iplus (x, itimes (n, d))))) → (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                       '(1 . 0),

cons (x, 0))))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (1, itimes (n, iplus (-1, c))), 0), cons (iplus (x, itimes (n, d)), 0)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; 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: iterk-e=1&x-iff-iterk e=1+ n c-1&x+nd-when-1<c&0<d&a>=x (ilessp (1, c) ∧ ilessp (0, d) ∧ (¬ ilessp (a, x)))

→ (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

 '(1 . 0),

cons (x, 0)))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (1, itimes (n (a, d, x), iplus (-1, c))),

0), cons (iplus (x, itimes (n (a, d, x), d)), 0))))

Theorem: iterk-exists-when-e=1+n c-1&x=x+nd&b<=0 ((¬ ilessp (0, b)) ∧ ilessp (1, c) ∧ ilessp (0, d)) → v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (1, itimes (n (a, d, x), iplus (-1, c))), 0), cons (iplus (x, itimes (n (a, d, x), d)), 0)))

Theorem: iterk-exists-when-x<=a&d>0&c<1&b<=0 ((¬ ilessp (0, b)) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ (¬ ilessp (a, x))) → v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

cons (x, 0)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; The next two events are versions of Part 5 of the
; Main Theorem given above in the introduction.
;  5. If  x <= a, d > 0, c > 1, and b <= 0, then
;     K( a,b,c,d,x ) exists.
;     Proof. By Lemma 7, the definition of the
;            function N, Part 1 of the Main Theorem,

;            and the definition of K.

Theorem: k-exists-when-x<=a&d>0&c<1&b<=0 ((¬ ilessp (0, b)) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ (¬ ilessp (a, x))) → v&c-apply$ ('k,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (x, 0)))

Theorem: k-halts-when-x<=a&d>0&c<1&b<=0 (vc-a ∧ vc-b ∧ vc-c ∧ vc-d ∧ vc-x ∧ (¬ ilessp (0, car (vc-b))) ∧ ilessp (1, car (vc-c)) ∧ ilessp (0, car (vc-d)) ∧ (¬ ilessp (car (vc-a), car (vc-x)))) → v&c-apply$ ('k, list (vc-a, vc-b, vc-c, vc-d, vc-x))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Lemma 8. Generalize Lemma 7 to the case when e > 1.
;  Assume 1 < c, 0 < d, 1 < e, 0 < n, and a+d >= x+nd.
;  Then
;  IterK( a,b,c,d,e,x ) exists
;   iff
;  IterK( a,b,c,d,e+n(c-1),x+nd ) exists
;  and
;  IterK( a,b,c,d,e,x )
;   =
;  IterK( a,b,c,d,e+n(c-1),x+nd ).
; Proof.  By Lemma 6 (with e2 = 1) and Lemma 7.

Theorem: x+-x+y=fix-int-y ilessp (0, x) → (iplus (x, iplus (− x, y)) = fix-int (y))

Theorem: fix-int-x=x-when-x>1 ilessp (1, x) → (fix-int (x) = x)

Theorem: iterk-e-x-iff-iterk-e-1-iterk-1-x ilessp (1, e) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0)))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e), 0), v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                  '(1 . 0),

cons (x, 0))))))

Theorem: iterk-e-x=iterk-e-1-iterk-1-x ilessp (1, e) → (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0))))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e), 0), v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                     '(1 . 0),

cons (x, 0)))))))

Theorem: iterk e+ n c-1&x+nd-exists-when-1<c&0<d&1<e&0<n&a+d>=x+nd-step-1 (ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (0, n) ∧ (¬ ilessp (iplus (a, d), iplus (x, itimes (n, d))))) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e), 0), v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                                '(1 . 0),

cons (x, 0)))))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e), 0), v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (1,

itimes (n,

iplus (-1, c))),

0), cons (iplus (x, itimes (n, d)), 0))))))

Theorem: iterk e+ n c-1&x+nd-value-when-1<c&0<d&1<e&0<n&a+d>=x+nd-step-1 (ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (0, n) ∧ (¬ ilessp (iplus (a, d), iplus (x, itimes (n, d))))) → (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e), 0), v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

              '(1 . 0),

cons (x, 0))))))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e), 0), v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (1,

itimes (n,

iplus (-1,

c))),

0), cons (iplus (x, itimes (n, d)),

0)))))))

Theorem: iterk e+ n c-1&x+nd-exists-when-1<c&0<d&1<e&0<n&a+d>=x+nd-step-2 (ilessp (1, c) ∧ ilessp (1, e) ∧ ilessp (0, n)) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e), 0), v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (1, itimes (n, iplus (-1, c))),

cons (iplus (x, itimes (n, d)), 0)))))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (e, itimes (n, iplus (-1, c))), 0), cons (iplus (x, itimes (n, d)), 0))))

Theorem: iterk e+ n c-1&x+nd-value-when-1<c&0<d&1<e&0<n&a+d>=x+nd-step-2 (ilessp (1, c) ∧ ilessp (1, e) ∧ ilessp (0, n)) → (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e), 0), v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (1,

itimes (n, iplus (-1, c))), 0),

cons (iplus (x, itimes (n, d)), 0))))))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (e, itimes (n, iplus (-1, c))), 0), cons (iplus (x, itimes (n, d)), 0)))))

Theorem: iterk e+ n c-1&x+nd-exists-when-1<c&0<d&1<e&0<n&a+d>=x+nd (ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (1, e) ∧ ilessp (0, n) ∧ (¬ ilessp (iplus (a, d), iplus (x, itimes (n, d))))) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0)))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (e, itimes (n, iplus (-1, c))), 0), cons (iplus (x, itimes (n, d)), 0))))

Theorem: iterk e+ n c-1&x+nd-value-when-1<c&0<d&1<e&0<n&a+d>=x+nd (ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (1, e) ∧ ilessp (0, n) ∧ (¬ ilessp (iplus (a, d), iplus (x, itimes (n, d))))) → (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0))))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (e, itimes (n, iplus (-1, c))), 0), cons (iplus (x, itimes (n, d)), 0)))))

Theorem: iterk-e&x-iff-iterk e+ n c-1&x+nd-when-1<c&0<d&a>=x&e>1 (ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (1, e) ∧ (¬ ilessp (a, x))) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0)))

↔ v&c-apply$ ('iterk, list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (e, itimes (n (a, d, x), iplus (-1, c))), 0), cons (iplus (x, itimes (n (a, d, x), d)), 0))))

Theorem: iterk-e&x=iterk e+ n c-1&x+nd-when-1<c&0<d&a>=x&e>1 (ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (1, e) ∧ (¬ ilessp (a, x))) → (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0))))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (e,

itimes (n (a, d, x), iplus (-1, c))), 0),

cons (iplus (x, itimes (n (a, d, x), d)), 0)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Lemma 9. The number of iterates of K can be reduced
;          by one if the value of x is reduced by b
;          when a < x.
;  Assume  1 < e, and  a < x.
;  Then
;  IterK( a,b,c,d,e,x ) exists
;   iff
;  IterK( a,b,c,d,e-1,x-b ) exists
;  and
;  IterK( a,b,c,d,e,x )
;   =
;  IterK( a,b,c,d,e-1,x-b ).

; Proof.  By Lemma 6 (with e2 = 1), and the definition
;         of IterK for values of x larger than a.

Theorem: iterk e x-iff-iterk e-1 x-b-when-1<e&x>a-step-1 (ilessp (a, x) ∧ ilessp (1, e)) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e), 0), v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

              '(1 . 0),

cons (x, 0)))))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e), 0), cons (idifference (x, b), 0))))

Theorem: iterk e x=iterk e-1 x-b-when-1<e&x>a-step-1 (ilessp (a, x) ∧ ilessp (1, e)) → (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e), 0), v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                  '(1 . 0),

cons (x, 0))))))

= car (v&c-apply$ ('iterk, list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e), 0), cons (idifference (x, b), 0)))))

Theorem: iterk e x-iff-iterk e-1 x-b-when-1<e&x>a (ilessp (a, x) ∧ ilessp (1, e)) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0)))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e), 0), cons (idifference (x, b), 0))))

Theorem: iterk e x=iterk e-1 x-b-when-1<e&x>a (ilessp (a, x) ∧ ilessp (1, e)) → (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0))))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e), 0), cons (idifference (x, b), 0)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Lemma 10. A key fact noted by Knuth in his proof.
;  Assume 1 < c, 0 < d, 1 < e, and  x <= a.

;  Then
;  IterK( a,b,c,d,e,x ) exists
;   iff
;  IterK( a,b,c,d,e-1+N( a,d,x )(c-1),x+N( a,d,x )d-b )
;  exists
;  and
;  IterK( a,b,c,d,e,x )
;   =
;  IterK( a,b,c,d,e-1+N( a,d,x )(c-1),x+N( a,d,x )d-b ).
; Proof.  By Lemma 8, the definition of the function N,
;         and Lemma 9.

Theorem: e+n c-1 >1-when-1<c&1<e&0<n (ilessp (1, c) ∧ ilessp (1, e) ∧ ilessp (0, n)) → ilessp (1, iplus (e, itimes (n, iplus (-1, c))))

Theorem: iterk-e&x-iff-iterk -1+e+ n c-1&x+nd-b-when-1<c&0<d&a>=x&e>1 (ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (1, e) ∧ (¬ ilessp (a, x))) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0)))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1,

iplus (e,

itimes (n (a, d, x), iplus (-1, c)))),

0), cons (idifference (iplus (x, itimes (n (a, d, x), d)),

b),

0))))

Theorem: iterk-e&x=iterk -1+e+ n c-1&x+nd-b-when-1<c&0<d&a>=x&e>1 (ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (1, e) ∧ (¬ ilessp (a, x)))

→ (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0))))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1,

iplus (e,

itimes (n (a, d, x),

iplus (-1, c)))),

0), cons (idifference (iplus (x,

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

0)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Lemma 11. Another key fact noted by Knuth.
;  Assume 0 < b, 1 < c, 0 < d, 1 < e, and  x <= a.
;  Then
;  IterK( a,b,c,d,e-1,x-b ) exists
;   iff
;  IterK( a,b,c,d,e-1+N( a,d,x )(c-1),x-b+N( a,d,x )d )
;  exists
;  and
;  IterK( a,b,c,d,e-1,x-b )
;   =
;  IterK( a,b,c,d,e-1+N( a,d,x )(c-1),x-b+N( a,d,x )d ).
; Proof.  By Lemma 7 (if e = 2), Lemma 8 (if e > 2), and
;         the definition of the function N.

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

Theorem: iterk-e-1&x-b-iff-iterk e-1+ n c-1&x-b+nd-when-1<c&0<d&a>=x&b>0&e>2 (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (2, e) ∧ (¬ ilessp (a, x))) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e), 0), cons (idifference (x, b), 0)))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1,

iplus (e,

itimes (n (a, d, x), iplus (-1, c)))),

0), cons (idifference (iplus (x, itimes (n (a, d, x), d)),

b),

0))))

Theorem: iterk-e-1&x-b=iterk e-1+ n c-1&x-b+nd-when-1<c&0<d&a>=x&e>2 (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (2, e) ∧ (¬ ilessp (a, x))) → (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e), 0),

cons (idifference (x, b), 0))))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1,

iplus (e,

itimes (n (a, d, x),

iplus (-1, c)))),

0), cons (idifference (iplus (x,

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

0)))))

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

Theorem: iterk-e-1&x-b-iff-iterk e-1+ n c-1&x-b+nd-when-1<c&0<d&a>=x&b>0&e=2 (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ (e = 2) ∧ (¬ ilessp (a, x))) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e), 0), cons (idifference (x, b), 0)))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1,

iplus (e,

itimes (n (a, d, x), iplus (-1, c)))),

0), cons (idifference (iplus (x, itimes (n (a, d, x), d)),

b),

0))))

Theorem: iterk-e-1&x-b=iterk e-1+ n c-1&x-b+nd-when-1<c&0<d&a>=x&b>0&e=2 (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ (e = 2) ∧ (¬ ilessp (a, x))) → (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e), 0), cons (idifference (x, b), 0))))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1,

iplus (e,

itimes (n (a, d, x),

iplus (-1, c)))),

0), cons (idifference (iplus (x,

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

0)))))

Theorem: iterk-e-1&x-b-iff-iterk e-1+ n c-1&x-b+nd-when-1<c&0<d&a>=x&b>0&e>1 (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (1, e) ∧ (¬ ilessp (a, x))) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e), 0), cons (idifference (x, b), 0)))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1,

iplus (e,

itimes (n (a, d, x), iplus (-1, c)))),

0), cons (idifference (iplus (x, itimes (n (a, d, x), d)),

b),

0))))

Theorem: iterk-e-1&x-b=iterk e-1+ n c-1&x-b+nd-when-1<c&0<d&a>=x&b>0&e>1 (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (1, e) ∧ (¬ ilessp (a, x))) → (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e), 0), cons (idifference (x, b), 0))))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1,

iplus (e,

itimes (n (a, d, x),

iplus (-1, c)))),

0), cons (idifference (iplus (x,

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

0)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Lemma 12. The number of iterates of K can be reduced
;           by one if the value of x is reduced by b
;           when a >= x and restrictions are placed
;           on the parameters a,b,c, and d.

;  Assume  0 < b, 1 < c, 0 < d, 1 < e, and  a >= x.
;  Then
;  IterK( a,b,c,d,e,x ) exists
;   iff
;  IterK( a,b,c,d,e-1,x-b ) exists
;  and
;  IterK( a,b,c,d,e,x )
;   =
;  IterK( a,b,c,d,e-1,x-b ).
; Proof.  By Lemma 10 and Lemma 11.

Theorem: iterk e x-iff-iterk e-1 x-b-when-0<b&1<c&0<d&1<e&a>=x (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (1, e) ∧ (¬ ilessp (a, x))) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0)))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e), 0), cons (idifference (x, b), 0))))

Theorem: iterk e x=iterk e-1 x-b-when-0<b&1<c&0<d&1<e&a>=x (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (1, e) ∧ (¬ ilessp (a, x)))

→ (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0))))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e), 0), cons (idifference (x, b), 0)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Lemma 13. Combine Lemma 9 and Lemma 12 about reducing
;           the number of iterates of K by one.
;  Assume  0 < b, 1 < c, 0 < d, and 1 < e.
;  Then
;  IterK( a,b,c,d,e,x ) exists
;   iff
;  IterK( a,b,c,d,e-1,x-b ) exists
;  and
;  IterK( a,b,c,d,e,x )
;   =
;  IterK( a,b,c,d,e-1,x-b ).
; Proof.  By Lemma 9 (if x > a) and Lemma 12 (if x <= a).

Theorem: iterk e x-iff-iterk e-1 x-b-when-0<b&1<c&0<d&1<e (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (1, e)) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0),

cons (x, 0)))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e), 0), cons (idifference (x, b), 0))))

Theorem: iterk e x=iterk e-1 x-b-when-0<b&1<c&0<d&1<e (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (1, e)) → (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0))))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (-1, e), 0), cons (idifference (x, b), 0)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Lemma 14. Generalize Lemma 13 by reducing the number
;           of iterates of K by more than one.
;  Assume  0 < b, 1 < c, 0 < d, 1 < e, and 0 < j < e.
;  Then
;  IterK( a,b,c,d,e,x ) exists
;   iff
;  IterK( a,b,c,d,e-j,x-jb ) exists
;  and
;  IterK( a,b,c,d,e,x )
;   =
;  IterK( a,b,c,d,e-j,x-jb ).

; Proof.  By induction on j.

Theorem: iterk e x-iff-iterk e-j x-jb-when-0<b&1<c&0<d&1<e&0<j<e (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (1, e) ∧ ilessp (0, j ) ∧ ilessp (j , e)) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0)))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (idifference (e, j ), 0), cons (idifference (x, itimes (b, j )), 0))))

Theorem: iterk e x=iterk e-j x-jb-when-0<b&1<c&0<d&1<e&0<j<e (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (1, e) ∧ ilessp (0, j ) ∧ ilessp (j , e)) → (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0))))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (idifference (e, j ), 0), cons (idifference (x, itimes (b, j )), 0)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Lemma 15. A special case of Lemma 14.
;  Assume  0 < b, 1 < c, 0 < d, and  a >= x.
;  Then
;  IterK( a,b,c,d,1,x ) exists
;   iff
;  IterK( a,b,c,d,1,x+d-(c-1)b ) exists
;  and
;  IterK( a,b,c,d,1,x )
;   =
;  IterK( a,b,c,d,1,x+d-(c-1)b ).
; Proof.  By Lemma 14 with e = c, j = c-1, and
;         x replaced by  x + d.

Theorem: iterk x-iff-iterk x+d c-1 b-when-0<b&1<c&0<d&a>=x (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ (¬ ilessp (a, x))) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                    '(1 . 0),

cons (x, 0)))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                        '(1 . 0),

cons (iplus (x,

idifference (d,

itimes (b, iplus (-1, c)))),

0))))

Theorem: iterk x=iterk x+d c-1 b-when-0<b&1<c&0<d&a>=x (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ (¬ ilessp (a, x))) → (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                       '(1 . 0),

cons (x, 0))))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                           '(1 . 0),

cons (iplus (x,

idifference (d,

itimes (b,

iplus (-1, c)))),

0)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; The next two events give a version of Part 6  of
; the Main Theorem given above in the introduction.
;  6. If  x <= a, d > 0, c > 1, and b > 0, then
;     K( a,b,c,d,x ) exists if and only if
;     K( a,b,c,d,x+d-(c-1)b )  exists and
;     K( a,b,c,d,x ) = K( a,b,c,d,x+d-(c-1)b ).
;     Proof. By Lemma 15 and the definition of K.

Theorem: k x-iff-k x+d c-1 b-when-0<b&1<c&0<d&a>=x (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ (¬ ilessp (a, x))) → (v&c-apply$ ('k,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (x, 0)))

↔ v&c-apply$ ('k,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (x,

idifference (d,

itimes (b, iplus (-1, c)))),

0))))

Theorem: k x=k x+d c-1 b-when-0<b&1<c&0<d&a>=x (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ (¬ ilessp (a, x))) → (car (v&c-apply$ ('k,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (x, 0))))

= car (v&c-apply$ ('k,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (x,

idifference (d,

itimes (b,

iplus (-1, c)))),

0)))))

Theorem: k x-iff-k x+d c-1 b-when-0<b&1<c&0<d&a>=x-version-2 (vc-a ∧ vc-b ∧ vc-c ∧ vc-d ∧ vc-x ∧ ilessp (0, car (vc-b)) ∧ ilessp (1, car (vc-c)) ∧ ilessp (0, car (vc-d)) ∧ (¬ ilessp (car (vc-a), car (vc-x)))) → (v&c-apply$ ('k, list (vc-a, vc-b, vc-c, vc-d, vc-x))

↔ v&c-apply$ ('k,

list (cons (car (vc-a), 0), cons (car (vc-b), 0), cons (car (vc-c), 0), cons (car (vc-d), 0), cons (iplus (car (vc-x),

idifference (car (vc-d),

itimes (car (vc-b),

iplus (-1,

car (vc-c))))),

0))))

Theorem: k x=k x+d c-1 b-when-0<b&1<c&0<d&a>=x-version-2 (vc-a ∧ vc-b ∧ vc-c ∧ vc-d ∧ vc-x ∧ ilessp (0, car (vc-b)) ∧ ilessp (1, car (vc-c)) ∧ ilessp (0, car (vc-d)) ∧ (¬ ilessp (car (vc-a), car (vc-x)))) → (car (v&c-apply$ ('k, list (vc-a, vc-b, vc-c, vc-d, vc-x)))

= car (v&c-apply$ ('k,

list (cons (car (vc-a), 0), cons (car (vc-b), 0), cons (car (vc-c), 0), cons (car (vc-d), 0), cons (iplus (car (vc-x),

idifference (car (vc-d),

itimes (car (vc-b),

iplus (-1,

car (vc-c))))),

0)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; The next two events give a more general version
; of Part 6  of the Main Theorem.

Theorem: k x-iff-k x+d c-1 b-when-0<b&1<c&0<d&a>=x-version-3 (vc-a ∧ vc-b ∧ vc-c ∧ vc-d ∧ vc-x ∧ ilessp (0, car (vc-b)) ∧ ilessp (1, car (vc-c)) ∧ ilessp (0, car (vc-d)) ∧ (¬ ilessp (car (vc-a), car (vc-x)))) → (v&c-apply$ ('k, list (vc-a, vc-b, vc-c, vc-d, vc-x))

↔ v&c-apply$ ('k,

list (vc-a, vc-b, vc-c, vc-d, cons (iplus (car (vc-x),

idifference (car (vc-d), itimes (car (vc-b),

iplus (-1,

car (vc-c))))),

cost))))

Theorem: k x=k x+d c-1 b-when-0<b&1<c&0<d&a>=x-version-3 (vc-a ∧ vc-b ∧ vc-c ∧ vc-d ∧ vc-x ∧ ilessp (0, car (vc-b)) ∧ ilessp (1, car (vc-c)) ∧ ilessp (0, car (vc-d)) ∧ (¬ ilessp (car (vc-a), car (vc-x)))) → (car (v&c-apply$ ('k, list (vc-a, vc-b, vc-c, vc-d, vc-x)))

= car (v&c-apply$ ('k,

list (vc-a, vc-b, vc-c, vc-d, cons (iplus (car (vc-x),

idifference (car (vc-d),

itimes (car (vc-b),

iplus (-1,

car (vc-c))))),

cost)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Lemma 16. The parameter c can be replaced by 1 if
;           the parameter d is modified in a suitable
;           way, when certain restrictions are placed
;           on the parameters.
;  Assume  0 < b, 1 < c, 0 < d, and  (c-1)b < d.
;  Then
;  IterK( a,b,c,d,1,x ) exists
;   iff
;  IterK( a,b,1,d-(c-1)b,1,x ) exists
;  and

;  IterK( a,b,c,d,1,x )
;   =
;  IterK( a,b,1,d-(c-1)b,1,x ).
; Proof.  By induction on the value given by
;         if  x > a  then  0
;                    else  1 + a - x.
;         Also use Lemma 15.

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

< k-measure (a, x))

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

elseif ilessp (a, x) then t

else induct-hint-1-k-measure (a, b, c, d, iplus (x,

idifference (d,

itimes (b,

iplus (-1, c))))) endif

Theorem: iterk c&d-iff-iterk 1&d-c-1 b-when-0<b&1<c&0<d&b c-1 <d (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (itimes (b, iplus (-1, c)), d)) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                    '(1 . 0),

cons (x, 0)))

↔ v&c-apply$ ('iterk, list (cons (a, 0), cons (b, 0),

                        '(1 . 0),

cons (idifference (d, itimes (b, iplus (-1, c))), 0),

                        '(1 . 0),

cons (x, 0))))

Theorem: iterk c&d=iterk 1&d-c-1 b-when-0<b&1<c&0<d&b c-1 <d (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (itimes (b, iplus (-1, c)), d)) → (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                       '(1 . 0),

cons (x, 0))))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0),

                           '(1 . 0),

cons (idifference (d, itimes (b, iplus (-1, c))),

0),

                           '(1 . 0),

cons (x, 0)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; The next two events give a version of Part 7  of
; the Main Theorem given above in the introduction.
;  7. If  d > 0, c > 1, b > 0, and (c-1)b < d, then
;     K( a,b,c,d,x )  exists if and only if
;     K( a,b,1,d-(c-1)b,x ) exists and
;     K( a,b,c,d,x ) = K( a,b,1,d-(c-1)b,x ).
;     Proof. By Lemma 16.

Theorem: k c&d-iff-k 1&d-c-1 b-when-0<b&1<c&0<d&b c-1 <d (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (itimes (b, iplus (-1, c)), d)) → (v&c-apply$ ('k,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (x, 0)))

↔ v&c-apply$ ('k,

list (cons (a, 0), cons (b, 0),

                      '(1 . 0),

cons (idifference (d, itimes (b, iplus (-1, c))), 0), cons (x, 0))))

Theorem: k c&d=k 1&d-c-1 b-when-0<b&1<c&0<d&b c-1 <d (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (itimes (b, iplus (-1, c)), d)) → (car (v&c-apply$ ('k,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (x, 0))))

= car (v&c-apply$ ('k,

list (cons (a, 0), cons (b, 0),

                         '(1 . 0),

cons (idifference (d, itimes (b, iplus (-1, c))),

0), cons (x, 0)))))

Theorem: k c&d-iff-k 1&d-c-1 b-when-0<b&1<c&0<d&b c-1 <d-version-2 (vc-a ∧ vc-b ∧ vc-c ∧ vc-d ∧ vc-x ∧ ilessp (0, car (vc-b)) ∧ ilessp (1, car (vc-c)) ∧ ilessp (0, car (vc-d)) ∧ ilessp (itimes (car (vc-b), iplus (-1, car (vc-c))), car (vc-d))) → (v&c-apply$ ('k, list (vc-a, vc-b, vc-c, vc-d, vc-x))

↔ v&c-apply$ ('k,

list (cons (car (vc-a), 0), cons (car (vc-b), 0),

                      '(1 . 0),

cons (idifference (car (vc-d), itimes (car (vc-b),

iplus (-1, car (vc-c)))),

0), cons (car (vc-x), 0))))

Theorem: k c&d=k 1&d-c-1 b-when-0<b&1<c&0<d&b c-1 <d-version-2 (vc-a ∧ vc-b ∧ vc-c ∧ vc-d ∧ vc-x ∧ ilessp (0, car (vc-b)) ∧ ilessp (1, car (vc-c)) ∧ ilessp (0, car (vc-d)) ∧ ilessp (itimes (car (vc-b), iplus (-1, car (vc-c))), car (vc-d))) → (car (v&c-apply$ ('k, list (vc-a, vc-b, vc-c, vc-d, vc-x)))

= car (v&c-apply$ ('k,

list (cons (car (vc-a), 0), cons (car (vc-b), 0),

                         '(1 . 0),

cons (idifference (car (vc-d),

itimes (car (vc-b),

iplus (-1,

car (vc-c)))),

0), cons (car (vc-x), 0)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; The next two events give a more general version
; of Part 7  of the Main Theorem.

Theorem: k c&d-iff-k 1&d-c-1 b-when-0<b&1<c&0<d&b c-1 <d-version-3 (vc-a ∧ vc-b ∧ vc-c ∧ vc-d ∧ vc-x ∧ ilessp (0, car (vc-b)) ∧ ilessp (1, car (vc-c)) ∧ ilessp (0, car (vc-d)) ∧ ilessp (itimes (car (vc-b), iplus (-1, car (vc-c))), car (vc-d))) → (v&c-apply$ ('k, list (vc-a, vc-b, vc-c, vc-d, vc-x))

↔ v&c-apply$ ('k,

list (vc-a, vc-b, cons (1, cost1 ), cons (idifference (car (vc-d),

itimes (car (vc-b),

iplus (-1, car (vc-c)))),

cost2 ), vc-x)))

Theorem: k c&d=k 1&d-c-1 b-when-0<b&1<c&0<d&b c-1 <d-version-3 (vc-a ∧ vc-b ∧ vc-c ∧ vc-d ∧ vc-x ∧ ilessp (0, car (vc-b)) ∧ ilessp (1, car (vc-c)) ∧ ilessp (0, car (vc-d)) ∧ ilessp (itimes (car (vc-b), iplus (-1, car (vc-c))), car (vc-d))) → (car (v&c-apply$ ('k, list (vc-a, vc-b, vc-c, vc-d, vc-x)))

= car (v&c-apply$ ('k,

list (vc-a, vc-b, cons (1, cost1 ), cons (idifference (car (vc-d),

itimes (car (vc-b),

iplus (-1,

car (vc-c)))),

cost2 ), vc-x))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Lemma 17. Essentially the if-part of Knuth's
;           theorem characterizing the parameters
;           when K is total.
;  Assume  0 < b, 1 < c, 0 < d, and  (c-1)b < d.
;  Then IterK( a,b,c,d,1,x ) exists.
; Proof.  By Lemma 4 and Lemma 16.

Theorem: iterk-exists-when-0<b&1<c&0<d&b c-1 <d (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d)

∧ ilessp (itimes (b, iplus (-1, c)), d)) → v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                 '(1 . 0),

cons (x, 0)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; The next two events are versions of Part 8  of the
; Main Theorem given above in the introduction.
;  8. If  d > 0, c > 1, b > 0, and (c-1)b < d, then
;     K( a,b,c,d,x ) exists.
;     Proof. By Lemma 17.

Theorem: k-exists-when-0<b&1<c&0<d&b c-1 <d (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (itimes (b, iplus (-1, c)), d)) → v&c-apply$ ('k,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (x, 0)))

Theorem: k-halts-when-0<b&1<c&0<d&b c-1 <d (vc-a ∧ vc-b ∧ vc-c ∧ vc-d ∧ vc-x ∧ ilessp (0, car (vc-b)) ∧ ilessp (1, car (vc-c)) ∧ ilessp (0, car (vc-d)) ∧ ilessp (itimes (car (vc-b), iplus (-1, car (vc-c))), car (vc-d))) → v&c-apply$ ('k, list (vc-a, vc-b, vc-c, vc-d, vc-x))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Lemma 18. The cost of computing K is lowered when d is
;           added to x.
;  Assume  1 < c, a >= x, and IterK( a,b,c,d,1,x ) exists.

;  Then IterK( a,b,c,d,1,x+d ) exists
;   and
;  cost[ IterK( a,b,c,d,1,x+d ) ]
;   <
;  cost[ IterK( a,b,c,d,1,x ) ]
; Proof. By the definition of IterK and Lemma 2.

Theorem: iterk-x+d-exists-when-iterk-exists&1<c&a>=x (ilessp (1, c) ∧ (¬ ilessp (a, x)) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

cons (x, 0))))

→ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

cons (iplus (d, x), 0)))

Theorem: iterk-x+d-cost<cost-iterk-when-iterk-exists&1<c&a>=x (ilessp (1, c) ∧ (¬ ilessp (a, x)) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

cons (x, 0))))

→ (cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                       '(1 . 0),

cons (iplus (d, x), 0))))

< cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                           '(1 . 0),

cons (x, 0)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Lemma 19. The cost of computing K is lowered
;           when K is iterated c times and
;           "enough" d's are added to x.
;  Assume  1 < c, a >= x, 0 < d, and
;  IterK( a,b,c,d,1,x ) exists.
;  Then IterK( a,b,c,d,c,x+N( a,d,x )d ) exists
;   and
;  cost[ IterK( a,b,c,d,c,x+N( a,d,x )d ) ]
;   <
;  cost[ IterK( a,b,c,d,1,x ) ]
; Proof. Hold a fixed and induct on the
;        value given by
;        if  x > a  then  0
;                   else  1 + a - x.

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

Definition: induct-hint-2-k-measure (a, d, x) = if ¬ ilessp (0, d) then t

elseif ilessp (a, x) then t

elseif ilessp (a, iplus (d, x)) then t

else induct-hint-2-k-measure (a, d, iplus (d, x)) endif

Theorem: iterk-x+nd-exists-when-iterk-exists&1<c&a>=x&0<d (ilessp (1, c) ∧ ilessp (0, d) ∧ (¬ ilessp (a, x)) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

cons (x, 0))))

→ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (c, 0), cons (iplus (x, itimes (d, n (a, d, x))), 0)))

Theorem: iterk-x+nd-cost<cost-iterk-when-iterk-exists&1<c&a>=x&0<d (ilessp (1, c) ∧ ilessp (0, d) ∧ (¬ ilessp (a, x)) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

cons (x, 0))))

→ (cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (c, 0), cons (iplus (x, itimes (d, n (a, d, x))), 0))))

< cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

        '(1 . 0),

cons (x, 0)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Lemma 20. The number of iterates of K can be
;           reduced to 1 if "enough" b's are
;           sutracted from x.
;  Assume  0 < b, 1 < c, 0 < d, 1 < e, 0 < i < e,
;  and IterK( a,b,c,d,e,x ) exists.
;  Then IterK( a,b,c,d,1,x-ib ) exists.
; Proof. By Lemma 14 and Lemma 2.

Theorem: e-i=1-when-1+i>=e&i<e ((¬ ilessp (iplus (1, i), e)) ∧ ilessp (i, e)) → (iplus (e, ineg (i)) = 1)

Theorem: iterk 1 x-ib-exists-when-iterk e x-exists&0<b&1<c&0<d&1<e&0<i<e (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (1, e) ∧ ilessp (0, i) ∧ ilessp (i, e) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0))))

→ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                   '(1 . 0),

cons (idifference (x, itimes (b, i)), 0)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Lemma 21. Another lemma reducing the number of
;           iterates of K and subtracting b's
;           from x.
;  Assume  0 < b, 1 < c, 0 < d, 0 < i, a+ib < x+b,
;  and IterK( a,b,c,d,i+1,x ) exists.

;  Then IterK( a,b,c,d,1,x-ib ) exists
;   and
;  cost[ IterK( a,b,c,d,1,x-ib ) ]
;   <
;  cost[ IterK( a,b,c,d,i+1,x ) ]
; Proof. By Lemma 20 (for the exists portion)
;        and induction on i (for the cost portion).

Theorem: iterk 1 x-ib cost<cost-iterk i+1 x-base-case (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ (i = 1) ∧ ilessp (iplus (a, itimes (b, i)), iplus (x, b)) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (1, i), 0), cons (x, 0))))

→ (cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                       '(1 . 0),

cons (idifference (x, itimes (b, i)), 0))))

< cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (1, i), 0), cons (x, 0)))))

Theorem: fix-int-x=x-when-0<x ilessp (0, x) → (fix-int (x) = x)

Theorem: iterk 1 x-ib cost<cost-iterk i+1 x-step-1 (ilessp (0, i)

∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (1, i), 0), cons (x, 0))))

→ (cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (i, 0), cons (x, 0))))))

< cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (1, i), 0), cons (x, 0)))))

Theorem: iterk i x-iff-iterk 1 x-ib-when-0<b&1<c&0<d&i>0&i<>1 (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (0, i) ∧ (i ≠ 1)) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (i, 0), cons (x, 0)))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

cons (iplus (x, ineg (itimes (b, iplus (-1, i)))), 0))))

Theorem: iterk i x=iterk 1 x-ib-when-0<b&1<c&0<d&i>0&i<>1 (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (0, i) ∧ (i ≠ 1)) → (car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (i, 0), cons (x, 0))))

= car (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

       '(1 . 0),

cons (iplus (x, ineg (itimes (b, iplus (-1, i)))), 0)))))

Theorem: iterk 1 x-ib cost<cost-iterk i+1 x-exists-step-2 (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (0, i) ∧ (i ≠ 1)) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (i, 0), cons (x, 0)))))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

    '(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                   '(1 . 0),

cons (iplus (x,

ineg (itimes (b,

iplus (-1,

i)))),

0))))))

Theorem: iterk 1 x-ib cost<cost-iterk i+1 x-step-2 (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (0, i) ∧ (i ≠ 1) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (i, 0), cons (x, 0)))))

∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

              '(1 . 0),

cons (iplus (x,

ineg (itimes (b,

iplus (-1, i)))),

0)))))

∧ (cdr (v&c-apply$ ('iterk, list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

cons (iplus (x, ineg (itimes (b, iplus (-1, i)))), 0))))

< cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (i, 0), cons (x, 0))))))

→ (cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

              '(1 . 0),

cons (iplus (x,

ineg (itimes (b,

iplus (-1,

i)))),

0))))))

< cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

    '(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (i, 0), cons (x, 0)))))))

Theorem: iterk i+1 exists-iff-iterk 1 iterk i exists (ilessp (0, i) ∧ (i ≠ 1)) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (1, i), 0), cons (x, 0)))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                      '(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (i, 0), cons (x, 0))))))

Theorem: iterk 1 x-ib cost<cost-iterk i+1 x-step-1&2 (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (0, i) ∧ (i ≠ 1) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (1, i), 0), cons (x, 0)))

∧ (cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                      '(1 . 0),

cons (iplus (x, ineg (itimes (b, iplus (-1, i)))), 0))))

< cdr (v&c-apply$ ('iterk, list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (i, 0), cons (x, 0))))))

→ (cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

              '(1 . 0),

cons (iplus (x,

ineg (itimes (b,

iplus (-1,

i)))),

0))))))

< cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (1, i), 0), cons (x, 0)))))

Theorem: iterk 1 x-ib cost<cost-iterk i+1 x-exists-step-3 (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (0, i) ∧ (i ≠ 1) ∧ ilessp (iplus (a, itimes (b, i)), iplus (x, b))) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

v&c-apply$ ('iterk, list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

               '(1 . 0),

cons (iplus (x,

ineg (itimes (b,

iplus (-1, i)))),

0)))))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

     '(1 . 0),

cons (iplus (x, ineg (itimes (b, i))), 0))))

Theorem: iterk 1 x-ib cost<cost-iterk i+1 x-step-3 (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (0, i) ∧ (i ≠ 1) ∧ ilessp (iplus (a, itimes (b, i)), iplus (x, b)) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

cons (iplus (x, ineg (itimes (b, i))), 0)))

∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

              '(1 . 0),

cons (iplus (x, ineg (itimes (b,

iplus (-1, i)))),

0))))))

→ (cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

cons (iplus (x, ineg (itimes (b, i))), 0))))

< cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

    '(1 . 0),

v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                  '(1 . 0),

cons (iplus (x,

ineg (itimes (b,

iplus (-1,

i)))),

0)))))))

Theorem: iterk i+1 x-iff-iterk 1 x-ib-when-0<b&1<c&0<d&i>0 (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (0, i)) → (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (1, i), 0), cons (x, 0)))

↔ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

cons (iplus (x, ineg (itimes (b, i))), 0))))

Theorem: iterk 1 x-ib cost<cost-iterk i+1 x-step-1&2&3 (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (0, i) ∧ (i ≠ 1) ∧ ilessp (iplus (a, itimes (b, i)), iplus (x, b)) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (1, i), 0), cons (x, 0)))

∧ (cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                      '(1 . 0),

cons (iplus (x, ineg (itimes (b, iplus (-1, i)))), 0))))

< cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (i, 0), cons (x, 0))))))

→ (cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                      '(1 . 0),

cons (iplus (x, ineg (itimes (b, i))), 0))))

< cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (1, i), 0), cons (x, 0)))))

Theorem: a+bi<x+b-when-a+bi<b+b+x&0<b (ilessp (0, b) ∧ ilessp (iplus (a, itimes (b, i)), iplus (x, b))) → ilessp (iplus (a, itimes (b, i)), iplus (b, iplus (b, x)))

Theorem: iterk-e=i-exists-when-iterk-e=i+1-exists (ilessp (0, i) ∧ (i ≠ 1) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (1, i), 0), cons (x, 0))))

→ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (i, 0), cons (x, 0)))

Theorem: iterk 1 x-ib cost<cost-iterk i+1 x-induction-step (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (0, i) ∧ (i ≠ 1) ∧ ilessp (iplus (a, itimes (b, i)), iplus (x, b)) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (1, i), 0), cons (x, 0)))

∧ ((ilessp (0, b)

∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (0, iplus (-1, i)) ∧ ilessp (iplus (a, itimes (b, iplus (-1, i))), iplus (x, b)) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (1, iplus (-1, i)), 0), cons (x, 0))))

→ (cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

cons (idifference (x,

itimes (b, iplus (-1, i))),

0))))

< cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (1, iplus (-1, i)), 0), cons (x, 0)))))))

→ (cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

cons (idifference (x, itimes (b, i)), 0))))

< cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (1, i), 0), cons (x, 0)))))

Theorem: iterk 1 x-ib cost<cost-iterk i+1 x (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (0, i) ∧ ilessp (iplus (a, itimes (b, i)), iplus (x, b)) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (1, i), 0), cons (x, 0))))

→ (cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                       '(1 . 0),

cons (idifference (x, itimes (b, i)), 0))))

< cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (iplus (1, i), 0), cons (x, 0)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Lemma 22. A generalization of Lemma 21.
;  Assume  0 < b, 1 < c, 0 < d, 0 < i, a+ib < x+b,
;  i < e, and IterK( a,b,c,d,e,x ) exists.
;  Then IterK( a,b,c,d,1,x-ib ) exists
;   and
;  cost[ IterK( a,b,c,d,1,x-ib ) ]
;   <
;  cost[ IterK( a,b,c,d,e,x ) ]
; Proof. Lemma 2 and Lemma 21.

Theorem: iterk 1 x-ib cost<cost-iterk e x-case-1 (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (0, i) ∧ ilessp (iplus (1, i), e) ∧ ilessp (iplus (a, itimes (b, i)), iplus (x, b)) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0))))

→ (cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

cons (idifference (x, itimes (b, i)), 0))))

< cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0)))))

Theorem: iterk 1 x-ib cost<cost-iterk e x-case-2 (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (0, i) ∧ (iplus (1, i) = e) ∧ ilessp (iplus (a, itimes (b, i)), iplus (x, b)) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0))))

→ (cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

cons (idifference (x, itimes (b, i)), 0))))

< cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0)))))

Theorem: e=i+1-or-e>i+1-when-e>i>0 (ilessp (0, i) ∧ ilessp (i, e)) → ((e = iplus (1, i)) ∨ ilessp (iplus (1, i), e))

Theorem: iterk 1 x-ib cost<cost-iterk e x (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (0, i) ∧ ilessp (i, e) ∧ ilessp (iplus (a, itimes (b, i)), iplus (x, b)) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0))))

→ (cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

cons (idifference (x, itimes (b, i)), 0))))

< cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (e, 0), cons (x, 0)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Define the function J( a,b,x ) recursively,
;  so that whenever b > 0, J( a,b,x ) is the smallest
;  nonnegative integer i such that x <= a + ib.

Definition: how-far-above-a (a, x) = if ¬ ilessp (a, x) then 0

else iplus (x, ineg (a)) endif

Theorem: numberp x-a when x>a ilessp (a, x) → (iplus (x, ineg (a)) ∈ N)

Theorem: x-a-b<x-a-when-0<b&a<x&a+b<x (ilessp (0, b) ∧ ilessp (a, x) ∧ ilessp (iplus (a, b), x)) → (iplus (x, iplus (ineg (a), ineg (b))) < iplus (x, ineg (a)))

Theorem: a<>x-when-a<x ilessp (a, x) → (fix-int (x) ≠ fix-int (a))

Definition: j (a, b, x) = if ¬ ilessp (0, b) then 0

elseif ¬ ilessp (a, x) then 0

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

Theorem: j>=0 ¬ ilessp (j (a, b, x), 0)

Theorem: j>0-when-x>a&b>0 (ilessp (0, b) ∧ ilessp (a, x)) → ilessp (0, j (a, b, x))

Theorem: x<=a+jb-when-0<b ilessp (0, b) → (¬ ilessp (iplus (a, itimes (b, j (a, b, x))), x))

Theorem: a+jb<x+b-when-0<b&a<x (ilessp (0, b) ∧ ilessp (a, x)) → ilessp (iplus (a, itimes (b, j (a, b, x))), iplus (b, x))

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

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

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Lemma 23. A special case of Lemma 22.

;  Assume  0 < b, 1 < c, 0 < d, a < x, a+(c-1)b >= x,
;  and IterK( a,b,c,d,c,x ) exists.
;  Then IterK( a,b,c,d,1,x-J( a,b,x )b ) exists
;   and
;  cost[ IterK( a,b,c,d,1,x-J( a,b,x )b ) ]
;   <
;  cost[ IterK( a,b,c,d,c,x ) ]
; Proof. By Lemma 22 and the definition of J.

Theorem: iterk 1 x-jb-exists-when-iterk e=c x-exists&0<b&1<c&0<d&etc (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (a, x) ∧ (¬ ilessp (iplus (a, itimes (b, iplus (-1, c))), x)) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (c, 0), cons (x, 0))))

→ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                   '(1 . 0),

cons (idifference (x, itimes (b, j (a, b, x))), 0)))

Theorem: iterk 1 x-jb cost<cost-iterk e=c x (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (a, x) ∧ (¬ ilessp (iplus (a, itimes (b, iplus (-1, c))), x)) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (c, 0), cons (x, 0))))

→ (cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                       '(1 . 0),

cons (idifference (x, itimes (b, j (a, b, x))), 0))))

< cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (c, 0), cons (x, 0)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Define the function L( a,b,d,x ) to be the following
;  combination of  x, b, d, and the functions J and N:
;     x + N( a,d,x ) d - J( a,b,x+N( a,d,x )d ) b.

Definition: l (a, b, d, x) = iplus (iplus (x, itimes (d, n (a, d, x))),

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

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Lemma 24. Computing K with L( a,b,d,x ) is cheaper
;           than computing K with x.
;  Assume  0 < b, 1 < c, 0 < d, a >= x, (c-1)b >= d,
;  and IterK( a,b,c,d,1,x ) exists.
;  Then IterK( a,b,c,d,1,L( a,b,d,x ) ) exists
;   and
;  cost[ IterK( a,b,c,d,1,L( a,b,d,x ) ) ]
;   <
;  cost[ IterK( a,b,c,d,1,x ) ]

; Proof. By Lemma 19 and Lemma 23.

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

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

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

Theorem: iterk-l-exists-when-iterk-x-exists&0<b&1<c&0<d&etc (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ (¬ ilessp (a, x)) ∧ (¬ ilessp (itimes (b, iplus (-1, c)), d)) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                  '(1 . 0),

cons (x, 0))))

→ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                 '(1 . 0),

cons (l (a, b, d, x), 0)))

Theorem: iterk-l-cost<cost-iterk-x&0<b&1<c&0<d-etc (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ (¬ ilessp (a, x)) ∧ (¬ ilessp (itimes (b, iplus (-1, c)), d)) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                   '(1 . 0),

cons (x, 0))))

→ (cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                       '(1 . 0),

cons (l (a, b, d, x), 0))))

< cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                           '(1 . 0),

cons (x, 0)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Define the function IterL( i,a,b,d,x ) which iterates
;  the function L i times.

Theorem: count x-1<count x-when-1<x ilessp (1, x) → (count (iplus (-1, x)) < count (x))

Definition: iterl (i, a, b, d, x) = if ilessp (1, i) then l (a, b, d, iterl (iplus (-1, i), a, b, d, x))

else l (a, b, d, x) endif

Theorem: l<=a ilessp (0, b) → (¬ ilessp (a, l (a, b, d, x)))

Event: Disable l.

Theorem: iterl<=a ilessp (0, b) → (¬ ilessp (a, iterl (i, a, b, d, x)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Lemma 25. The cost of computing K is unbounded
;           when (c-1)b >= d
;  Assume  0 < b, 1 < c, 0 < d, a >= x, (c-1)b >= d,
;  i > 0, and IterK( a,b,c,d,1,x ) exists.

;  Then IterK( a,b,c,d,1,IterL( i,a,b,d,x ) ) exists
;   and
;  cost[ IterK( a,b,c,d,1,IterL( i,a,b,d,x ) ) ] + i-1
;   <
;  cost[ IterK( a,b,c,d,1,x ) ]
; Proof. By induction on i using Lemma 24.

Theorem: iterk-iterl-exists-when-iterk-x-exists&0<b&1<c&0<d&etc (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (0, i) ∧ (¬ ilessp (a, x)) ∧ (¬ ilessp (itimes (b, iplus (-1, c)), d)) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                   '(1 . 0),

cons (x, 0))))

→ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                   '(1 . 0),

cons (iterl (i, a, b, d, x), 0)))

Theorem: fix-int-cost=cost fix-int (cdr (v&c-apply$ (fn, args))) = cdr (v&c-apply$ (fn, args))

Theorem: x+i-1<z-when-x<y&-1-1+i+y<z ((x < y) ∧ (iplus (-1, iplus (-1, iplus (i, y))) < z)) → (iplus (-1, iplus (i, x)) < z)

Theorem: iterk-iterl-cost+i-1<cost-iterk-x&0<b&1<c&0<d-etc-induction-step (ilessp (0, i) ∧ (i ≠ 1) ∧ (iplus (-1, iplus (-1,

iplus (i,

cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                                     '(1 . 0),

cons (iterl (iplus (-1, i), a, b, d, x),

0)))))))

< cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                          '(1 . 0),

cons (x, 0)))))

∧ ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ (¬ ilessp (a, x)) ∧ (¬ ilessp (itimes (b, c), iplus (b, d))) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                  '(1 . 0),

cons (x, 0))))

→ (iplus (-1,

iplus (i,

cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                                '(1 . 0),

cons (l (a, b, d,

iterl (iplus (-1, i), a, b, d, x)), 0))))))

< cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

cons (x, 0)))))

Theorem: iterk-iterl-cost+i-1<cost-iterk-x&0<b&1<c&0<d-etc (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (0, i) ∧ (¬ ilessp (a, x)) ∧ (¬ ilessp (itimes (b, iplus (-1, c)), d)) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

cons (x, 0))))

→ (iplus (-1,

iplus (i,

cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

      '(1 . 0),

cons (iterl (i, a, b, d, x), 0))))))

< cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

'(1 . 0),

cons (x, 0)))))

Theorem: i<y-when-0<x&-1+i+x<y ((0 < x) ∧ (iplus (-1, iplus (i, x)) < y)) → (i < y)

Event: Disable iterl.

Theorem: iterk-cost-is-unbounded-when- c-1 b>=d&x<=a&etc (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ ilessp (0, i) ∧ (¬ ilessp (a, x)) ∧ (¬ ilessp (itimes (b, iplus (-1, c)), d)) ∧ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                  '(1 . 0),

cons (x, 0))))

→ (i < cdr (v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                         '(1 . 0),

cons (x, 0)))))

Theorem: iterk-does-not-exist-when- c-1 b>=d&x<=a&etc (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ (¬ ilessp (a, x)) ∧ (¬ ilessp (itimes (b, iplus (-1, c)), d))) → (¬ v&c-apply$ ('iterk,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0),

                    '(1 . 0),

cons (x, 0))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; The next two events are versions of Part 9 of the
; Main Theorem given above in the introduction.
;  9. If  x <= a, d > 0, c > 1, b > 0, and
;     (c-1)b >= d, then K( a,b,c,d,x ) does
;     not exist.

;     Proof. By Lemma 25 and the definition of K.

Theorem: k-does-not-exist-when- c-1 b>=d&x<=a&etc (ilessp (0, b) ∧ ilessp (1, c) ∧ ilessp (0, d) ∧ (¬ ilessp (a, x)) ∧ (¬ ilessp (itimes (b, iplus (-1, c)), d))) → (¬ v&c-apply$ ('k,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (x, 0))))

Theorem: k-does-not-halt-when- c-1 b>=d&x<=a&etc (vc-a ∧ vc-b ∧ vc-c ∧ vc-d ∧ vc-x ∧ ilessp (0, car (vc-b)) ∧ ilessp (1, car (vc-c)) ∧ ilessp (0, car (vc-d)) ∧ (¬ ilessp (car (vc-a), car (vc-x))) ∧ (¬ ilessp (itimes (car (vc-b), iplus (-1, car (vc-c))), car (vc-d)))) → (¬ v&c-apply$ ('k, list (vc-a, vc-b, vc-c, vc-d, vc-x)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Here a quantifier is used to define the concept that K
; is a total function of x with parameters a,b,c, and d.
; This is the only place in this file of events that
; an explicit quantifier is used.

Definition: k-is-total (vc-a, vc-b, vc-c, vc-d) ↔ ∀ vc-x (vc-x → v&c-apply$ ('k, list (vc-a, vc-b, vc-c, vc-d, vc-x)))

Theorem: k-is-total-suff (vc-x (vc-a, vc-b, vc-c, vc-d) → v&c-apply$ ('k, list (vc-a, vc-b, vc-c, vc-d, vc-x (vc-a, vc-b, vc-c, vc-d)))) → k-is-total (vc-a, vc-b, vc-c, vc-d)

Theorem: k-is-total-necc (¬ (vc-x → v&c-apply$ ('k, list (vc-a, vc-b, vc-c, vc-d, vc-x)))) → (¬ k-is-total (vc-a, vc-b, vc-c, vc-d))

Event: Disable k.

Event: Disable k-is-total.

Theorem: knuth-theorem-if-part-case-1 (vc-a ∧ vc-b ∧ vc-c ∧ vc-d ∧ ilessp (0, car (vc-b)) ∧ ilessp (1, car (vc-c)) ∧ ilessp (0, car (vc-d))) → (ilessp (itimes (car (vc-b), iplus (-1, car (vc-c))), car (vc-d))

→ k-is-total (vc-a, vc-b, vc-c, vc-d))

Theorem: knuth-theorem-if-part-case-2 (vc-a ∧ vc-b ∧ vc-c ∧ vc-d ∧ ilessp (0, car (vc-b)) ∧ (¬ ilessp (1, car (vc-c))) ∧ ilessp (0, car (vc-d))) → (ilessp (itimes (car (vc-b), iplus (-1, car (vc-c))), car (vc-d))

→ k-is-total (vc-a, vc-b, vc-c, vc-d))

Theorem: knuth-theorem-if-part (vc-a ∧ vc-b ∧ vc-c ∧ vc-d ∧ ilessp (0, car (vc-b)) ∧ ilessp (0, car (vc-d))) → (ilessp (itimes (car (vc-b), iplus (-1, car (vc-c))), car (vc-d))

→ k-is-total (vc-a, vc-b, vc-c, vc-d))

Theorem: knuth-theorem-only-if-part-case-1 (vc-a ∧ vc-b ∧ vc-c ∧ vc-d ∧ ilessp (0, car (vc-b)) ∧ ilessp (1, car (vc-c)) ∧ ilessp (0, car (vc-d))) → (k-is-total (vc-a, vc-b, vc-c, vc-d)

→ ilessp (itimes (car (vc-b), iplus (-1, car (vc-c))), car (vc-d)))

Theorem: knuth-theorem-only-if-part-case-2 (ilessp (0, b) ∧ (¬ ilessp (1, c)) ∧ ilessp (0, d)) → ilessp (itimes (b, iplus (-1, c)), d)

Theorem: knuth-theorem-only-if-part (vc-a ∧ vc-b ∧ vc-c ∧ vc-d ∧ ilessp (0, car (vc-b)) ∧ ilessp (0, car (vc-d))) → (k-is-total (vc-a, vc-b, vc-c, vc-d)

→ ilessp (itimes (car (vc-b), iplus (-1, car (vc-c))), car (vc-d)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Here is a version of Knuth's theorem:
; 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.

Theorem: knuth-theorem (vc-a ∧ vc-b ∧ vc-c ∧ vc-d ∧ ilessp (0, car (vc-b)) ∧ ilessp (0, car (vc-d))) → (k-is-total (vc-a, vc-b, vc-c, vc-d)

↔ ilessp (itimes (car (vc-b), iplus (-1, car (vc-c))), car (vc-d)))

Theorem: k-value-when-a<x ilessp (a, x) → (car (v&c-apply$ ('k,

list (cons (a, 0), cons (b, 0), cons (c, 0), cons (d, 0), cons (x, 0))))

= idifference (x, b))

Theorem: k-value-when-a<x-version-2 (vc-a ∧ vc-b ∧ vc-c ∧ vc-d ∧ vc-x ∧ ilessp (car (vc-a), car (vc-x))) → (car (v&c-apply$ ('k, list (vc-a, vc-b, vc-c, vc-d, vc-x)))

= idifference (car (vc-x), car (vc-b)))

Theorem: knuth-theorem-part-2-case-1 (vc-a ∧ vc-b ∧ vc-c ∧ vc-d ∧ vc-x ∧ ilessp (0, car (vc-b)) ∧ ilessp (1, car (vc-c)) ∧ ilessp (0, car (vc-d))) → (car (v&c-apply$ ('k, list (vc-a, vc-b, vc-c, vc-d, vc-x)))

= if ilessp (car (vc-a), car (vc-x)) then idifference (car (vc-x), car (vc-b)) else car (v&c-apply$ ('k,

list (vc-a, vc-b, vc-c, vc-d, cons (iplus (car (vc-x),

idifference (car (vc-d),

itimes (car (vc-b),

iplus (-1,

car (vc-c))))),

cost)))) endif)

Theorem: k-value=body-value-when-a>=x&c=1 (¬ ilessp (a, x)) → (car (v&c-apply$ ('k,

list (cons (a, 0), cons (b, 0),

'(1 . 0),

cons (d, 0), cons (x, 0))))

= car (v&c-apply$ ('k,

list (cons (a, 0), cons (b, 0),

    '(1 . 0),

cons (d, 0),

cons (iplus (x, d), 0)))))

Theorem: k-value=body-value-when-a>=x&c=1-version-2 (vc-a ∧ vc-b ∧ vc-c ∧ vc-d ∧ vc-x ∧ (car (vc-c) = 1) ∧ (¬ ilessp (car (vc-a), car (vc-x)))) → (car (v&c-apply$ ('k, list (vc-a, vc-b, vc-c, vc-d, vc-x)))

= car (v&c-apply$ ('k,

list (vc-a, vc-b, vc-c, vc-d, cons (iplus (car (vc-x), car (vc-d)), cost)))))

Theorem: knuth-theorem-part-2-case-2 (vc-a ∧ vc-b ∧ vc-c ∧ vc-d ∧ vc-x ∧ (car (vc-c) = 1)) → (car (v&c-apply$ ('k, list (vc-a, vc-b, vc-c, vc-d, vc-x)))

= if ilessp (car (vc-a), car (vc-x)) then idifference (car (vc-x), car (vc-b)) else car (v&c-apply$ ('k,

list (vc-a, vc-b, vc-c, vc-d, cons (iplus (car (vc-x),

idifference (car (vc-d),

itimes (car (vc-b),

iplus (-1,

car (vc-c))))),

cost)))) endif)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Here is a version of that part of Knuth's theorem
; which gives the circumstances when K satisfies a
; simpler recurrence.
; Theorem.  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 ).

Theorem: knuth-theorem-part-2 (vc-a ∧ vc-b ∧ vc-c ∧ vc-d ∧ vc-x ∧ ilessp (0, car (vc-b)) ∧ ilessp (0, car (vc-c)) ∧ ilessp (0, car (vc-d))) → (car (v&c-apply$ ('k, list (vc-a, vc-b, vc-c, vc-d, vc-x)))

= if ilessp (car (vc-a), car (vc-x)) then idifference (car (vc-x), car (vc-b)) else car (v&c-apply$ ('k,

list (vc-a, vc-b, vc-c, vc-d, cons (iplus (car (vc-x),

idifference (car (vc-d),

itimes (car (vc-b),

iplus (-1,

car (vc-c))))),

cost)))) endif)

Index

a<>x-when-a<x, 102 a<-b+x-when-a<x&b<=0, 36 a<x+nd, 51 a>=x-when-a+d>=x+d, 45 a+ c-1 b>=x+nd-when-0<d&

a>=x& c-1 b>=d, 105 a+b<x-when-a<x&b<=0, 36 a+bi<x+b-when-a+bi<b+b+x&0

<b, 97 a+d>=x+ n-1 d-when-a+d>=x

+nd&0<d&0<n, 50 a+d>=x+nd-when-d>0&a>=x, 51 a+d>=x-b+nd-when-b>0&a+d>

=x+nd&d>0, 64 a+jb<x+b-when-0<b&a<x, 102 args-exist-when-fn-exists, 12

cost>0-if-fn-exists, 6 cost>cost-of-args, 27 cost>member, 28 cost-base-step-when-x<=a&d<

=0&c<=1, 23 cost-induction-step-when-x<=a

&d<=0&c<=1, 22

&d<=0&c>1, 31

cost-is-a-numberp, 6 cost-iterk-at-e1<cost-iterk-at

-e2-when-0<e1<e2, 28

-e2-when-0<e1<e2-basic-step, 28 count-sub1-x<count-x-when-x>

0&x<>1, 21 count-sub1-y<count-y-when-0<

x<y, 26 count x-1<count x-when-1<

x, 106

e+n c-1 >1-when-1<c&1<e

&0<n, 62 e-i=1-when-1+i>=e&i<e, 86 e=i+1-or-e>i+1-when-e>i>0, 101 eq-args-cost-depends-on-cost-of

-args, 10 eq-args-give-eq-existence, 10 eq-args-give-eq-values, 10

fix-int, 53, 87, 102, 107 fix-int-cost=cost, 107 fix-int-x=x-when-0<x, 87 fix-int-x=x-when-x>1, 53 forall, 111

how-far-above-a, 101, 102

i<y-when-0<x&-1+i+x<y, 109 idifference, 10–17, 36, 60–81, 86, 87,

98–101, 103, 104, 114–116 ilessp, 8, 9, 11–40, 44–62, 64–90, 92– 103, 105–116

ilessp-0-add1-x, 25

induct-hint-1-k-measure, 77 induct-hint-2-k-measure, 84 induct-hint-cost-hom, 26 induct-hint-k-measure, 34 induct-hint-positive-int, 21 ineg, 34, 36, 77, 86, 88–96, 102, 104 iplus, 19, 21–24, 26–32, 34, 36–70,

72–116 iplus 1 -1 x=x when x>0, 37 iterk, 4 iterk-at-e1-exists-when-iterk-at -e2-exists&0<e1<e2, 27 -e2-exists&0<e1<e2-basic-step,

27 iterk-cost>body-cost, 7 iterk-cost>body-cost-when-e<

=1&a>=x, 18

=1&a>=x-version-2, 19 iterk-cost>body-cost-when-e>

1-version-2, 13

1, 9 iterk-cost-is-unbounded-when-

c-1 b>=d&x<=a&etc, 110 iterk-cost-is-unbounded-when-x<

=a&d<=0&c<=1, 24 =a&d<=0&c>1, 32

iterk-does-not-exist-when- c-1

b>=d&x<=a&etc, 110 iterk-does-not-exist-when-x<=

a&d<=0&c<=1, 25 a&d<=0&c>1, 33

iterk-e-1&x-b-iff-iterk e-1+

n c-1&x-b+nd-when-1<c&0<d&a>=x&b>0&e>1,

66 n c-1&x-b+nd-when-1<c&0<d&a>=x&b>0&e>2,

64 n c-1&x-b+nd-when-1<c&0<d&a>=x&b>0&e=2,

65 iterk-e-1&x-b=iterk e-1+ n

c-1&x-b+nd-when-1<c&0<d&a>=x&b>0&e>1,

67 c-1&x-b+nd-when-1<c&0<d&a>=x&b>0&e=2,

66 c-1&x-b+nd-when-1<c&0<d&a>=x&e>2,

64 iterk-e-x-iff-iterk-e-1-iterk-1

-x, 54 iterk-e-x=iterk-e-1-iterk-1-x, 54 iterk-e=1&x-cost>i-1+cost-ite

rk-e=c&x+id-when-x<=a&d<=0&c<=1,

24 iterk-e=1&x-iff-iterk e=1+ n

c-1&x+nd-when-1<c&0<d&a>=x,

51 iterk-e=1&x-implies-iterk-e=c&

x+id-when-x<=a&d<=0&c<=1,

22 iterk-e=i-exists-when-iterk-e=i

+1-exists, 97 iterk-e&x-iff-iterk -1+e+ n

c-1&x+nd-b-when-1<c&0<d&a>=x&e>1,

62 iterk-e&x-iff-iterk e+ n c-

1&x+nd-when-1<c&0<d&a>=x&e>1,

58 iterk-e&x=iterk -1+e+ n c-1 &x+nd-b-when-1<c&0<d&a>=x&e>1,

62 iterk-e&x=iterk e+ n c-1&x

+nd-when-1<c&0<d&a>=x&e>1,

59 iterk-exists-iff-body-exists, 4 iterk-exists-iff-body-exists-whe

n-e<=1&a>=x, 17 n-e<=1&a>=x-version-2, 18 n-e>1, 8 n-e>1-version-2, 11 n-e>1-version-3, 14 n-e>1-version-3-case-1, 13 n-e>1-version-3-case-2, 14

iterk-exists-when-0<b&1<c&

0<d&b c-1 <d, 81 iterk-exists-when-d>0&c<=1

&e=c, 34 iterk-exists-when-e<=1&a<x, 16

-version-2, 36 iterk-exists-when-e=1+n c-1&x

=x+nd&b<=0, 52 iterk-exists-when-x<=a&d>0

&c<1&b<=0, 52 &c<=1&e=1, 35

iterk-exists&iterk>a-when-x>

a&b<=0&e>0, 36 iterk-iterl-cost+i-1<cost-ite

rk-x&0<b&1<c&0<d-etc, 109 rk-x&0<b&1<c&0<d-etc-induction-

step, 107 iterk-iterl-exists-when-iterk-x

-exists&0<b&1<c&0<d&etc, 107 iterk-l-cost<cost-iterk-x&0<

b&1<c&0<d-etc, 105 iterk-l-exists-when-iterk-x-exi

sts&0<b&1<c&0<d&etc, 105 iterk-v&c-apply$-idifference-

cost, 11 iterk-v&c-apply$-idifference-e

xists, 10 iterk-v&c-apply$-idifference-v

alue, 11 iterk-value-when-e<=1&a<x, 17 iterk-value-when-e<=1&a<x-ve

rsion-2, 36 iterk-value=body-value, 5 iterk-value=body-value-when-e<

=1&a>=x, 17 =1&a>=x-version-2, 19

iterk-value=body-value-when-e> 1-version-2, 12 1-version-3, 16 1-version-3-case-1, 15 1-version-3-case-2, 15 1, 8

iterk-x+d-cost<cost-iterk-whe

n-iterk-exists&1<c&a>=x, 83 iterk-x+d-cost<cost-iterk-x-w

hen-a>=x&1<c, 30 iterk-x+d-exists-when-iterk-exi

sts&1<c&a>=x, 83 iterk-x+nd-cost<cost-iterk-whe

n-iterk-exists&1<c&a>=x&0<d,

85 iterk-x+nd-exists-when-iterk-exi

sts&1<c&a>=x&0<d, 85 iterk-x-cost>i+cost-iterk-x+i

d-when-x<=a&d<=0&c>1&e=1,

32 iterk-x-implies-iterk-x+id-when

-x<=a&d<=0&c>1&e=1, 30 iterk 1 x-ib-exists-when-iter

k e x-exists&0<b&1<c&0<d&1<e&0<i<e,

86 iterk 1 x-ib cost<cost-ite

rk e x, 101 rk e x-case-1, 99 rk e x-case-2, 100 rk i+1 x, 98 rk i+1 x-base-case, 87 rk i+1 x-exists-step-2, 89 rk i+1 x-exists-step-3, 93 rk i+1 x-induction-step, 97 rk i+1 x-step-1, 87 rk i+1 x-step-1&2, 92 rk i+1 x-step-1&2&3, 96 rk i+1 x-step-2, 90

rk i+1 x-step-3, 94 iterk 1 x-jb-exists-when-iter

k e=c x-exists&0<b&1<c&0<d&etc,

103 iterk 1 x-jb cost<cost-ite rk e=c x, 103 iterk c&d-iff-iterk 1&d-c-1

b-when-0<b&1<c&0<d&b c-1 <d,

77 iterk c&d=iterk 1&d-c-1 b-

when-0<b&1<c&0<d&b c-1 <d,

78 iterk e+ n c-1&x+nd-exists-

when-1<c&0<d&1<e&0<n&a+d>=x+nd,

57 when-1<c&0<d&1<e&0<n&a+d>=x+nd-

step-1, 55 when-1<c&0<d&1<e&0<n&a+d>=x+nd-

step-2, 56 iterk e+ n c-1&x+nd-value-w

hen-1<c&0<d&1<e&0<n&a+d>=x+nd,

58 hen-1<c&0<d&1<e&0<n&a+d>=x+nd-

step-1, 55 hen-1<c&0<d&1<e&0<n&a+d>=x+nd-

step-2, 57 iterk e=1+ n c-1&x+nd-exist

s-base-step, 45 s-step-1, 46 s-step-2, 47 s-step-3, 49 s-when-1<c&0<d&0<n&a+d>=x+nd,

50 iterk e=1+ n c-1&x+nd-value

-base-step, 46 -step-1, 47 -step-2, 48 -step-3, 49 -when-1<c&0<d&0<n&a+d>=x+nd,

50 iterk e x-iff-iterk e-1 x-b

-when-0<b&1<c&0<d&1<e, 69 -when-0<b&1<c&0<d&1<e&a>=x,

68 -when-1<e&x>a, 61 -when-1<e&x>a-step-1, 60

iterk e x-iff-iterk e-j x-j

b-when-0<b&1<c&0<d&1<e&0<j<e,

71 iterk e x=iterk e-1 x-b-whe

n-0<b&1<c&0<d&1<e, 70 n-0<b&1<c&0<d&1<e&a>=x,

68 n-1<e&x>a, 61 n-1<e&x>a-step-1, 60

iterk e x=iterk e-j x-jb-whe

n-0<b&1<c&0<d&1<e&0<j<e,

71 iterk i+1 exists-iff-iterk 1

iterk i exists, 92 iterk i+1 x-iff-iterk 1 x-i

b-when-0<b&1<c&0<d&i>0, 95 iterk i x-iff-iterk 1 x-ib-

when-0<b&1<c&0<d&i>0&i<>1,

88 iterk i x=iterk 1 x-ib-when

-0<b&1<c&0<d&i>0&i<>1, 89 iterk x+ i-1 d implies ite

rk x+id-when-x<=a&d<=0&c<=1&i>0,

21 rk x+id-when-x<=a&d<=0&c>1&i>0&e=1,

29 iterk x-iff-iterk x+d c-1 b

-when-0<b&1<c&0<d&a>=x,

72 iterk x=iterk x+d c-1 b-whe

n-0<b&1<c&0<d&a>=x, 73 iterl, 106–109 iterl<=a, 106 itimes, 21–24, 29–32, 45–52, 55–59,

62–67, 71–82, 85–105, 107– 116

j, 102–104 j<c-when-0<b&a<x&c>1&

a+ c-1 b>=x, 102 j>0-when-x>a&b>0, 102 j>=0, 102 k, 4 k-does-not-exist-when- c-1 b>

=d&x<=a&etc, 111 k-does-not-exist-when-x<=a&d

<=0&c<=1, 25

<=0&c>1, 33

k-does-not-halt-when- c-1 b>

=d&x<=a&etc, 111 k-does-not-halt-when-x<=a&d<

=0&c<=1, 26

=0&c>1, 33

k-exists-when-0<b&1<c&0<

d&b c-1 <d, 82 k-exists-when-x<=a&d>0&c<

=1, 35

1&b<=0, 53 k-exists-when-x>a, 20 k-halts-when-0<b&1<c&0<

d&b c-1 <d, 82 k-halts-when-x<=a&d>0&c<

=1, 35

1&b<=0, 53 k-halts-when-x>a, 20 k-is-total, 111–113 k-is-total-necc, 112 k-is-total-suff, 111 k-measure, 34, 77 k-measure x+d<k-measure x-w

hen-0<d&a>=x, 34 k-measure x+d- c-1 b<k-mea

sure x-when- c-1 b<d&a>=x, 77 k-value-when-a<x, 113 k-value-when-a<x-version-2, 114 k-value=body-value-when-a>=x&

c=1, 114

c=1-version-2, 115 k c&d-iff-k 1&d-c-1 b-when

-0<b&1<c&0<d&b c-1 <d, 78 -0<b&1<c&0<d&b c-1 <d-version-

2, 79 -0<b&1<c&0<d&b c-1 <d-version-

3, 80 k c&d=k 1&d-c-1 b-when-0<

b&1<c&0<d&b c-1 <d, 79 b&1<c&0<d&b c-1 <d-version-

2, 80 b&1<c&0<d&b c-1 <d-version-

3, 81 k x-iff-k x+d c-1 b-when-0<

b&1<c&0<d&a>=x, 73

b&1<c&0<d&a>=x-version-2,

74 b&1<c&0<d&a>=x-version-3,

75 k x=k x+d c-1 b-when-0<b&

1<c&0<d&a>=x, 74

1<c&0<d&a>=x-version-2, 74 1<c&0<d&a>=x-version-3, 76

knuth-theorem, 113 knuth-theorem-if-part, 112 knuth-theorem-if-part-case-1, 112 knuth-theorem-if-part-case-2, 112 knuth-theorem-only-if-part, 113 knuth-theorem-only-if-part-case

-1, 112 -2, 113

knuth-theorem-part-2, 116 knuth-theorem-part-2-case-1, 114 knuth-theorem-part-2-case-2, 115

l, 104–106, 109 l<=a, 106

n, 51, 52, 59, 62–67, 84, 85, 104, 105 n>0-when-d>o&x<=a, 51 n>=0, 51 n-1 c-1>0-when-1<c&0<n&

n<>1, 46 n=1-when-x+d>a&a>=x&d>0, 84 n c-1 +1=c-when-n=1&c>1, 45 nbr-of-iterates-sum-exists-step

-1, 37 -2, 39 -3, 40

nbr-of-iterates-sum-exists&val

ues, 44 nbr-of-iterates-sum-values-step

-1, 38 -2, 40 -3, 42

nd=d-when-n=1&d>0, 45 numberp x-a when x>a, 102

sub1-x>0-when-x>0&x<>1, 21 sum-cdrs>=member, 27

v&c-apply$-if, 8

vc-x, 111

w-1+y<z&x<y-implies-w+x< z, 22

x<=a+jb-when-0<b, 102 x<y-1-when-0<x&x<y&x<

>y-1, 27 x<z-when-x<y&y<=z, 102 x>1-when-x>0&x<>1, 36 x>=z-when-x>=y&y>=z, 105 x+-x+y=fix-int-y, 53 x+2-1=x+1, 65 x+ i-1 d<=a-when-x<=a&d<

=0&i>0, 21 x+i-1<z-when-x<y&-1-1+i+y<

z, 107 x+y>1-when-x>0&x<>1&0

<y, 37 x-a-b<x-a-when-0<b&a<x&

a+b<x, 102

y<=z-when-x+y-1<z&x>=0&

y>0, 24 y>1-when-y>x&x>0, 26