Meeting a Challenge of Knuth John Cowles CLI and University of Wyoming September 1993 (work actually completed in the summer of 1991) This work was supported in part at Computational Logic, Inc., by the Defense Advanced Research Projects Agency, ARPA Order 7406. The views and conclusions contained in this document are those of the author(s) and should not be interpreted as representing the official policies, either expressed or implied, of Computational Logic, Inc., the Defense Advanced Research Projects Agency or the U.S. Government. This note presents two solutions to a challenge problem posed by Donald E. Knuth. It is the concatenation of files in the CLI directory /slocal/src/pc-nqthm-1992/examples/cowles/, to be released with Pc-Nqthm-1992. The organization is follows. 1. The file /slocal/src/pc-nqthm-1992/examples/cowles/knuth-91.events, which presents a solution using the Nqthm-1992 interpreter functions (e.g., EVAL$). 2. The file /slocal/src/pc-nqthm-1992/examples/cowles/knuth-91a.events, which presents a solution using the ``functional variables'' mechanism (CONSTRAIN and FUNCTIONALLY-INSTANTIATE events) of Nqthm-1992. 3. Supporting files of events, which need to be executed in the following order before running either of the two files above (which are each to be run independently on top of "integers"). a. bags.events b. naturals.events c. integers.events The paper referred to below has been published since the time that the events below were created. Here is the reference. D.E. Knuth, Textbook examples of recursion, In: Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, edited by V. Lifschitz, Academic Press, San Diego, CA, 1991, pages 207-229. ========================= knuth-91.events ========================= ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; 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. (NOTE-LIB "integers") ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; Define the partial function IterK using EVAL$, ; and define the partial function K using IterK. (DEFN 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)))) (DEFN 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. (PROVE-LEMMA ITERK-EXISTS-IFF-BODY-EXISTS (REWRITE) (IFF (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)))))))))) ; hint ( (EXPAND (V&C-APPLY$ 'ITERK (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS E 0) (CONS X 0)))) )) (PROVE-LEMMA ITERK-VALUE=BODY-VALUE (REWRITE) (EQUAL (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))))))))))) ; hint ( (EXPAND (V&C-APPLY$ 'ITERK (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS E 0) (CONS X 0)))) )) (PROVE-LEMMA COST-IS-A-NUMBERP (REWRITE GENERALIZE) (NUMBERP (CDR (V&C-APPLY$ FN ARGS))) ; hint ( (ENABLE V&C-APPLY$) )) (PROVE-LEMMA COST>0-IF-FN-EXISTS (REWRITE) (IMPLIES (V&C-APPLY$ FN ARGS) (LESSP 0 (CDR (V&C-APPLY$ FN ARGS)))) ; hint ( (ENABLE V&C-APPLY$) )) (PROVE-LEMMA ITERK-COST>BODY-COST (REWRITE) (IMPLIES (V&C-APPLY$ 'ITERK (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS E 0) (CONS X 0))) (LESSP (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)))))) ; hint ( (EXPAND (V&C-APPLY$ 'ITERK (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS E 0) (CONS X 0)))) )) (PROVE-LEMMA V&C-APPLY$-IF ( REWRITE ) (EQUAL (V&C-APPLY$ 'IF ARGS) (IF (CAR ARGS) (IF (CAAR ARGS) (FIX-COST (CADR ARGS) (ADD1 (CDAR ARGS))) (FIX-COST (CADDR ARGS) (ADD1 (CDAR ARGS)))) F)) ; hint ( (ENABLE V&C-APPLY$) )) (PROVE-LEMMA ITERK-EXISTS-IFF-BODY-EXISTS-WHEN-E>1 (REWRITE) (IMPLIES (ILESSP 1 E) (IFF (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)))))))) (PROVE-LEMMA ITERK-VALUE=BODY-VALUE-WHEN-E>1 (REWRITE) (IMPLIES (ILESSP 1 E) (EQUAL (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))))))))) (PROVE-LEMMA ITERK-COST>BODY-COST-WHEN-E>1 (REWRITE) (IMPLIES (AND (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)))) (LESSP (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)))))) ; hint ( (USE (ITERK-COST>BODY-COST (A A))) )) (PROVE-LEMMA EQ-ARGS-GIVE-EQ-EXISTENCE (REWRITE) (IMPLIES (AND (NOT (EQUAL FN 'QUOTE)) (NOT (EQUAL FN 'IF)) (EQUAL (STRIP-CARS ARGS1) (STRIP-CARS ARGS2)) (EQUAL (MEMBER F ARGS1) (MEMBER F ARGS2))) (IFF (V&C-APPLY$ FN ARGS1) (V&C-APPLY$ FN ARGS2))) ; hint ( (ENABLE V&C-APPLY$) )) (PROVE-LEMMA EQ-ARGS-GIVE-EQ-VALUES (REWRITE) (IMPLIES (AND (NOT (EQUAL FN 'QUOTE)) (NOT (EQUAL FN 'IF)) (EQUAL (STRIP-CARS ARGS1) (STRIP-CARS ARGS2)) (EQUAL (MEMBER F ARGS1) (MEMBER F ARGS2))) (EQUAL (CAR (V&C-APPLY$ FN ARGS1)) (CAR (V&C-APPLY$ FN ARGS2)))) ; hint ( (ENABLE V&C-APPLY$) )) (PROVE-LEMMA EQ-ARGS-COST-DEPENDS-ON-COST-OF-ARGS (REWRITE) (IMPLIES (AND (NOT (EQUAL FN 'IF)) (LESSP (SUM-CDRS ARGS1) (SUM-CDRS ARGS2)) (EQUAL (STRIP-CARS ARGS1) (STRIP-CARS ARGS2)) (V&C-APPLY$ FN ARGS1) (V&C-APPLY$ FN ARGS2)) (LESSP (CDR (V&C-APPLY$ FN ARGS1)) (CDR (V&C-APPLY$ FN ARGS2)))) ; hint ( (ENABLE V&C-APPLY$) )) (PROVE-LEMMA ITERK-V&C-APPLY$-IDIFFERENCE-EXISTS (REWRITE) (IFF (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)))) ; hint ( (USE (EQ-ARGS-GIVE-EQ-EXISTENCE (FN 'ITERK) (ARGS1 (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))) (ARGS2 (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS (IDIFFERENCE E 1) 0) (CONS X 0))))) )) (PROVE-LEMMA ITERK-V&C-APPLY$-IDIFFERENCE-VALUE (REWRITE) (EQUAL (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))))) ; hint ( (USE (EQ-ARGS-GIVE-EQ-VALUES (FN 'ITERK) (ARGS1 (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))) (ARGS2 (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS (IDIFFERENCE E 1) 0) (CONS X 0))))) )) (PROVE-LEMMA ITERK-V&C-APPLY$-IDIFFERENCE-COST (REWRITE) (IMPLIES (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))) (LESSP (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)))))) ; hint ( (USE (EQ-ARGS-COST-DEPENDS-ON-COST-OF-ARGS (FN 'ITERK) (ARGS2 (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))) (ARGS1 (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS (IDIFFERENCE E 1) 0) (CONS X 0))))) )) (PROVE-LEMMA ITERK-EXISTS-IFF-BODY-EXISTS-WHEN-E>1-VERSION-2 (REWRITE) (IMPLIES (ILESSP 1 E) (IFF (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))))))) ; hint ( (USE (EQ-ARGS-GIVE-EQ-EXISTENCE (FN 'ITERK) (ARGS1 (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))))) (ARGS2 (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))))))) (DISABLE ITERK-EXISTS-IFF-BODY-EXISTS) )) (PROVE-LEMMA ITERK-VALUE=BODY-VALUE-WHEN-E>1-VERSION-2 (REWRITE) (IMPLIES (ILESSP 1 E) (EQUAL (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)))))))) ; hint ( (USE (EQ-ARGS-GIVE-EQ-VALUES (FN 'ITERK) (ARGS1 (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))))) (ARGS2 (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))))))) (DISABLE ITERK-EXISTS-IFF-BODY-EXISTS) )) (PROVE-LEMMA ARGS-EXIST-WHEN-FN-EXISTS (REWRITE) (IMPLIES (AND (NOT (EQUAL FN 'IF)) (V&C-APPLY$ FN ARGS)) (NOT (MEMBER F ARGS))) ; hint ( (ENABLE V&C-APPLY$) )) (PROVE-LEMMA ITERK-COST>BODY-COST-WHEN-E>1-VERSION-2 (REWRITE) (IMPLIES (AND (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)))) (LESSP (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)))))) ; hint ( (USE (ARGS-EXIST-WHEN-FN-EXISTS (FN 'ITERK) (ARGS (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)))))) (ITERK-COST>BODY-COST-WHEN-E>1 (A A)) (ITERK-V&C-APPLY$-IDIFFERENCE-COST (A A)) (EQ-ARGS-GIVE-EQ-EXISTENCE (FN 'ITERK) (ARGS1 (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))))) (ARGS2 (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)))))) (EQ-ARGS-COST-DEPENDS-ON-COST-OF-ARGS (FN 'ITERK) (ARGS2 (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))))) (ARGS1 (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))))))) (DISABLE ITERK-EXISTS-IFF-BODY-EXISTS ITERK-VALUE=BODY-VALUE ARGS-EXIST-WHEN-FN-EXISTS) )) (PROVE-LEMMA ITERK-EXISTS-IFF-BODY-EXISTS-WHEN-E>1-VERSION-3-CASE-1 NIL (IMPLIES (AND VC-X (ILESSP 1 E)) (IFF (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)))))) ; hint ( (DISABLE ITERK-EXISTS-IFF-BODY-EXISTS ITERK-VALUE=BODY-VALUE) (USE (EQ-ARGS-GIVE-EQ-EXISTENCE (FN 'ITERK) (ARGS1 (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS E 0) VC-X)) (ARGS2 (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS E 0) (CONS (CAR VC-X) 0)))) (EQ-ARGS-GIVE-EQ-EXISTENCE (FN 'ITERK) (ARGS1 (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 (CAR VC-X) 0))))) (ARGS2 (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))))) (EQ-ARGS-GIVE-EQ-EXISTENCE (FN 'ITERK) (ARGS1 (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS (IDIFFERENCE E 1) 0) (CONS (CAR VC-X) 0))) (ARGS2 (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS (IDIFFERENCE E 1) 0) VC-X))) (EQ-ARGS-GIVE-EQ-VALUES (FN 'ITERK) (ARGS1 (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS (IDIFFERENCE E 1) 0) (CONS (CAR VC-X) 0))) (ARGS2 (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS (IDIFFERENCE E 1) 0) VC-X)))) )) (PROVE-LEMMA ITERK-EXISTS-IFF-BODY-EXISTS-WHEN-E>1-VERSION-3-CASE-2 NIL (IMPLIES (AND (EQUAL VC-X F) (ILESSP 1 E)) (IFF (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)))))) ; hint ( (ENABLE V&C-APPLY$) )) (PROVE-LEMMA ITERK-EXISTS-IFF-BODY-EXISTS-WHEN-E>1-VERSION-3 (REWRITE) (IMPLIES (ILESSP 1 E) (IFF (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)))))) ; hint ( (USE (ITERK-EXISTS-IFF-BODY-EXISTS-WHEN-E>1-VERSION-3-CASE-1 (A A)) (ITERK-EXISTS-IFF-BODY-EXISTS-WHEN-E>1-VERSION-3-CASE-2 (A A))) )) (PROVE-LEMMA ITERK-VALUE=BODY-VALUE-WHEN-E>1-VERSION-3-CASE-1 NIL (IMPLIES (AND VC-X (ILESSP 1 E)) (EQUAL (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))))))) ; hint ( (DISABLE ITERK-EXISTS-IFF-BODY-EXISTS ITERK-VALUE=BODY-VALUE) (USE (EQ-ARGS-GIVE-EQ-VALUES (FN 'ITERK) (ARGS1 (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS E 0) VC-X)) (ARGS2 (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS E 0) (CONS (CAR VC-X) 0)))) (EQ-ARGS-GIVE-EQ-VALUES (FN 'ITERK) (ARGS1 (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 (CAR VC-X) 0))))) (ARGS2 (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))))) (EQ-ARGS-GIVE-EQ-EXISTENCE (FN 'ITERK) (ARGS1 (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS (IDIFFERENCE E 1) 0) (CONS (CAR VC-X) 0))) (ARGS2 (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS (IDIFFERENCE E 1) 0) VC-X))) (EQ-ARGS-GIVE-EQ-VALUES (FN 'ITERK) (ARGS1 (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS (IDIFFERENCE E 1) 0) (CONS (CAR VC-X) 0))) (ARGS2 (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS (IDIFFERENCE E 1) 0) VC-X)))) )) (PROVE-LEMMA ITERK-VALUE=BODY-VALUE-WHEN-E>1-VERSION-3-CASE-2 NIL (IMPLIES (AND (EQUAL VC-X F) (ILESSP 1 E)) (EQUAL (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))))))) ; hint ( (ENABLE V&C-APPLY$) )) (PROVE-LEMMA ITERK-VALUE=BODY-VALUE-WHEN-E>1-VERSION-3 (REWRITE) (IMPLIES (ILESSP 1 E) (EQUAL (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))))))) ; hint ( (USE (ITERK-VALUE=BODY-VALUE-WHEN-E>1-VERSION-3-CASE-1 (A A)) (ITERK-VALUE=BODY-VALUE-WHEN-E>1-VERSION-3-CASE-2 (A A))) )) (PROVE-LEMMA ITERK-EXISTS-WHEN-E<=1&A=X (REWRITE) (IMPLIES (AND (NOT (ILESSP 1 E)) (NOT (ILESSP A X))) (IFF (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)))))))) (PROVE-LEMMA ITERK-VALUE=BODY-VALUE-WHEN-E<=1&A>=X (REWRITE) (IMPLIES (AND (NOT (ILESSP 1 E)) (NOT (ILESSP A X))) (EQUAL (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))))))))) (PROVE-LEMMA ITERK-COST>BODY-COST-WHEN-E<=1&A>=X (REWRITE) (IMPLIES (AND (NOT (ILESSP 1 E)) (NOT (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)))) (LESSP (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)))))) ; hint ( (USE (ITERK-COST>BODY-COST (A A))) )) (DISABLE ITERK-EXISTS-IFF-BODY-EXISTS) (DISABLE ITERK-VALUE=BODY-VALUE) (DISABLE ITERK-COST>BODY-COST) (PROVE-LEMMA ITERK-EXISTS-IFF-BODY-EXISTS-WHEN-E<=1&A>=X-VERSION-2 (REWRITE) (IMPLIES (AND (NOT (ILESSP 1 E)) (NOT (ILESSP A X))) (IFF (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))))) ; hint ( (USE (EQ-ARGS-GIVE-EQ-EXISTENCE (FN 'ITERK) (ARGS1 (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))))) (ARGS2 (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS C 0) (CONS (IPLUS X D) 0))))) )) (PROVE-LEMMA ITERK-VALUE=BODY-VALUE-WHEN-E<=1&A>=X-VERSION-2 (REWRITE) (IMPLIES (AND (NOT (ILESSP 1 E)) (NOT (ILESSP A X))) (EQUAL (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)))))) ; hint ( (USE (EQ-ARGS-GIVE-EQ-VALUES (FN 'ITERK) (ARGS1 (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))))) (ARGS2 (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS C 0) (CONS (IPLUS X D) 0))))) )) (PROVE-LEMMA ITERK-COST>BODY-COST-WHEN-E<=1&A>=X-VERSION-2 (REWRITE) (IMPLIES (AND (NOT (ILESSP 1 E)) (NOT (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)))) (LESSP (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)))))) ; hint ( (USE (ITERK-COST>BODY-COST-WHEN-E<=1&A>=X (A A)) (EQ-ARGS-COST-DEPENDS-ON-COST-OF-ARGS (FN 'ITERK) (ARGS2 (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))))) (ARGS1 (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS C 0) (CONS (IPLUS X D) 0)))) (EQ-ARGS-GIVE-EQ-EXISTENCE (FN 'ITERK) (ARGS1 (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))))) (ARGS2 (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS C 0) (CONS (IPLUS X D) 0))))) )) (DISABLE ITERK-EXISTS-IFF-BODY-EXISTS-WHEN-E>1) (DISABLE ITERK-VALUE=BODY-VALUE-WHEN-E>1) (DISABLE ITERK-COST>BODY-COST-WHEN-E>1) (DISABLE ITERK-EXISTS-IFF-BODY-EXISTS-WHEN-E<=1&A>=X) (DISABLE ITERK-VALUE=BODY-VALUE-WHEN-E<=1&A>=X) (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. (PROVE-LEMMA K-EXISTS-WHEN-X>A (REWRITE) (IMPLIES (ILESSP A X) (V&C-APPLY$ 'K (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS X 0)))) ; hint ( (expand (V&C-APPLY$ 'K (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS X 0)))) )) (PROVE-LEMMA K-HALTS-WHEN-X>A (REWRITE) (IMPLIES (AND 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 ))) ; hint ( (USE (EQ-ARGS-GIVE-EQ-EXISTENCE (FN 'K) (ARGS1 (LIST (CONS (CAR VC-A) 0) (CONS (CAR VC-B) 0) (CONS (CAR VC-C) 0) (CONS (CAR VC-D) 0) (CONS (CAR VC-X) 0))) (ARGS2 (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. (PROVE-LEMMA COUNT-SUB1-X0&X<>1 (REWRITE) (IMPLIES (AND (ILESSP 0 X) (NOT (EQUAL X 1))) (LESSP (COUNT (IPLUS -1 X)) (COUNT X))) ; hint ( (DISABLE-THEORY INTEGERS NATURALS) (ENABLE-THEORY INTEGER-DEFNS) )) (DEFN INDUCT-HINT-POSITIVE-INT ( X ) (IF (NOT (ILESSP 0 X)) T (IF (EQUAL X 1) T (INDUCT-HINT-POSITIVE-INT (IPLUS -1 X))))) (PROVE-LEMMA SUB1-X>0-WHEN-X>0&X<>1 (REWRITE) (IMPLIES (AND (ILESSP 0 X) (NOT (EQUAL X 1))) (ILESSP 0 (IPLUS -1 X))) ; hint ( (DISABLE-THEORY INTEGERS NATURALS) (ENABLE-THEORY INTEGER-DEFNS) )) (PROVE-LEMMA X+_I-1_D<=A-WHEN-X<=A&D<=0&I>0 (REWRITE) (IMPLIES (AND (NOT (ILESSP A X)) (NOT (ILESSP 0 D)) (ILESSP 0 I)) (NOT (ILESSP A (IPLUS X (ITIMES (IPLUS -1 I) D))))) ; hint ( (DISABLE-THEORY INTEGERS) (ENABLE-THEORY INTEGER-DEFNS) )) (PROVE-LEMMA ITERK_X+_I-1_D_IMPLIES_ITERK_X+ID-WHEN-X<=A&D<=0&C<=1&I>0 (REWRITE) (IMPLIES (AND (NOT (ILESSP A X)) (NOT (ILESSP 0 D)) (NOT (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)))) ; hint ( (USE (ITERK-EXISTS-IFF-BODY-EXISTS-WHEN-E<=1&A>=X-VERSION-2 (E C)(X (IPLUS X (ITIMES (IPLUS -1 I) D)))) (X+_I-1_D<=A-WHEN-X<=A&D<=0&I>0 (A A))) )) (PROVE-LEMMA ITERK-E=1&X-IMPLIES-ITERK-E=C&X+ID-WHEN-X<=A&D<=0&C<=1 (REWRITE) (IMPLIES (AND (NOT (ILESSP A X)) (NOT (ILESSP 0 D)) (NOT (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)))) ; hint ( (INDUCT (INDUCT-HINT-POSITIVE-INT I)) )) (PROVE-LEMMA W-1+Y0 (A A)) (ITERK-E=1&X-IMPLIES-ITERK-E=C&X+ID-WHEN-X<=A&D<=0&C<=1 (I (IPLUS -1 I))) (ITERK-COST>BODY-COST-WHEN-E<=1&A>=X-VERSION-2 (E C) (X (IPLUS X (ITIMES (IPLUS -1 I) D))))) )) (PROVE-LEMMA COST-BASE-STEP-WHEN-X<=A&D<=0&C<=1 (REWRITE) (IMPLIES (AND (NOT (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)))) (LESSP (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)))))) ; hint ( (USE (ITERK-COST>BODY-COST-WHEN-E<=1&A>=X-VERSION-2 (E 1))) )) (PROVE-LEMMA ITERK-E=1&X-COST>I-1+COST-ITERK-E=C&X+ID-WHEN-X<=A&D<=0&C<=1 (REWRITE) (IMPLIES (AND (NOT (ILESSP A X)) (NOT (ILESSP 0 D)) (NOT (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)))) (LESSP (PLUS (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)))))) ; hint ( (INDUCT (INDUCT-HINT-POSITIVE-INT I)) )) (PROVE-LEMMA Y<=Z-WHEN-X+Y-1=0&Y>0 NIL (IMPLIES (AND (NUMBERP X) (ILESSP 0 Y) (LESSP (PLUS X (IPLUS -1 Y)) Z)) (EQUAL (NOT (LESSP Z Y)) T)) ; hint ( (DISABLE-THEORY INTEGERS NATURALS) (ENABLE-THEORY INTEGER-DEFNS) )) (PROVE-LEMMA ITERK-COST-IS-UNBOUNDED-WHEN-X<=A&D<=0&C<=1 (REWRITE) (IMPLIES (AND (NOT (ILESSP A X)) (NOT (ILESSP 0 D)) (NOT (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)))) (NOT (LESSP (CDR (V&C-APPLY$ 'ITERK (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) '(1 . 0) (CONS X 0)))) I))) ; hint ( (USE (Y<=Z-WHEN-X+Y-1=0&Y>0 (X (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))))) (Y I) (Z (CDR (V&C-APPLY$ 'ITERK (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) '(1 . 0) (CONS X 0))))))) )) (PROVE-LEMMA ILESSP-0-ADD1-X (REWRITE) (ILESSP 0 (ADD1 X)) ; hint ( (DISABLE-THEORY INTEGERS NATURALS) (ENABLE-THEORY INTEGER-DEFNS) )) (PROVE-LEMMA ITERK-DOES-NOT-EXIST-WHEN-X<=A&D<=0&C<=1 (REWRITE) (IMPLIES (AND (NOT (ILESSP A X)) (NOT (ILESSP 0 D)) (NOT (ILESSP 1 C))) (NOT (V&C-APPLY$ 'ITERK (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) '(1 . 0) (CONS X 0))))) ; hint ( (USE (ITERK-COST-IS-UNBOUNDED-WHEN-X<=A&D<=0&C<=1 (I (ADD1 (CDR (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. (PROVE-LEMMA K-DOES-NOT-EXIST-WHEN-X<=A&D<=0&C<=1 (REWRITE) (IMPLIES (AND (NOT (ILESSP A X)) (NOT (ILESSP 0 D)) (NOT (ILESSP 1 C))) (NOT (V&C-APPLY$ 'K (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS X 0))))) ; hint ( (EXPAND (V&C-APPLY$ 'K (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS X 0)))) )) (PROVE-LEMMA K-DOES-NOT-HALT-WHEN-X<=A&D<=0&C<=1 (REWRITE) (IMPLIES (AND VC-A VC-B VC-C VC-D VC-X (NOT (ILESSP (CAR VC-A)(CAR VC-X))) (NOT (ILESSP 0 (CAR VC-D))) (NOT (ILESSP 1 (CAR VC-C)))) (NOT (V&C-APPLY$ 'K (LIST VC-A VC-B VC-C VC-D VC-X)))) ; hint ( (USE (EQ-ARGS-GIVE-EQ-EXISTENCE (FN 'K) (ARGS1 (LIST (CONS (CAR VC-A) 0) (CONS (CAR VC-B) 0) (CONS (CAR VC-C) 0) (CONS (CAR VC-D) 0) (CONS (CAR VC-X) 0))) (ARGS2 (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. (PROVE-LEMMA COUNT-SUB1-Y1-WHEN-Y>X&X>0 (REWRITE) (IMPLIES (AND (ILESSP 0 X) (ILESSP X Y)) (ILESSP 1 Y)) ; hint ( (DISABLE-THEORY INTEGERS NATURALS) (ENABLE-THEORY INTEGER-DEFNS) )) (PROVE-LEMMA ITERK-AT-E1-EXISTS-WHEN-ITERK-AT-E2-EXISTS&0Y-1 (REWRITE) (IMPLIES (AND (ILESSP 0 X) (ILESSP X Y) (NOT (EQUAL X (IPLUS -1 Y)))) (ILESSP X (IPLUS -1 Y))) ; hint ( (DISABLE-THEORY INTEGERS NATURALS) (ENABLE-THEORY INTEGER-DEFNS) )) (PROVE-LEMMA ITERK-AT-E1-EXISTS-WHEN-ITERK-AT-E2-EXISTS&01-WHEN-Y>X&X>0) )) (PROVE-LEMMA COST>COST-OF-ARGS (REWRITE) (IMPLIES (AND (NOT (EQUAL FN 'IF)) (NOT (MEMBER F ARGS)) (V&C-APPLY$ FN ARGS)) (LESSP (SUM-CDRS ARGS) (CDR (V&C-APPLY$ FN ARGS)))) ; hint ( (ENABLE V&C-APPLY$) )) (PROVE-LEMMA SUM-CDRS>=MEMBER (REWRITE) (IMPLIES (MEMBER X L) (NOT (LESSP (SUM-CDRS L)(CDR X))))) (PROVE-LEMMA COST>MEMBER (REWRITE) (IMPLIES (AND (V&C-APPLY$ FN ARGS) (NOT (EQUAL FN 'IF)) (MEMBER X ARGS) ) (LESSP (CDR X) (CDR (V&C-APPLY$ FN ARGS))))) (PROVE-LEMMA COST-ITERK-AT-E1MEMBER (FN 'ITERK) (ARGS (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 E2) 0) (CONS X 0))))) (X (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))))) (ITERK-COST>BODY-COST-WHEN-E>1-VERSION-2 (E E2))) )) (DISABLE Y>1-WHEN-Y>X&X>0) (PROVE-LEMMA COST-ITERK-AT-E1 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. (PROVE-LEMMA ITERK_X+_I-1_D_IMPLIES_ITERK_X+ID-WHEN-X<=A&D<=0&C>1&I>0&E=1 (REWRITE) (IMPLIES (AND (NOT (ILESSP A X)) (NOT (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)))) ; hint ( (USE (ITERK-EXISTS-IFF-BODY-EXISTS-WHEN-E<=1&A>=X-VERSION-2 (E 1)(X (IPLUS X (ITIMES (IPLUS -1 I) D)))) (X+_I-1_D<=A-WHEN-X<=A&D<=0&I>0 (A A))) )) (PROVE-LEMMA ITERK-X-IMPLIES-ITERK-X+ID-WHEN-X<=A&D<=0&C>1&E=1 (REWRITE) (IMPLIES (AND (NOT (ILESSP A X)) (NOT (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)))) ; hint ( (INDUCT (INDUCT-HINT-POSITIVE-INT I)) )) (PROVE-LEMMA ITERK-X+D-COST=X&11 (REWRITE) (IMPLIES (AND (NOT (ILESSP A X)) (NOT (ILESSP 0 D)) (ILESSP 1 C) (ILESSP 0 I) (NOT (EQUAL I 1)) (V&C-APPLY$ 'ITERK (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) '(1 . 0) (CONS X 0))) (LESSP (PLUS (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)))))) (LESSP (PLUS (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)))))) ; hint ( (USE (X+_I-1_D<=A-WHEN-X<=A&D<=0&I>0 (A A)) (ITERK-X-IMPLIES-ITERK-X+ID-WHEN-X<=A&D<=0&C>1&E=1 (I (IPLUS -1 I))) (ITERK-X+D-COST=X&1I+COST-ITERK-X+ID-WHEN-X<=A&D<=0&C>1&E=1 (REWRITE) (IMPLIES (AND (NOT (ILESSP A X)) (NOT (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)))) (LESSP (PLUS (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)))))) ; hint ( (INDUCT (INDUCT-HINT-POSITIVE-INT I)) )) (PROVE-LEMMA ITERK-COST-IS-UNBOUNDED-WHEN-X<=A&D<=0&C>1 (REWRITE) (IMPLIES (AND (NOT (ILESSP A X)) (NOT (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)))) (LESSP I (CDR (V&C-APPLY$ 'ITERK (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) '(1 . 0) (CONS X 0)))))) ; hint ( (USE (ITERK-X-COST>I+COST-ITERK-X+ID-WHEN-X<=A&D<=0&C>1&E=1 (A A))) )) (PROVE-LEMMA ITERK-DOES-NOT-EXIST-WHEN-X<=A&D<=0&C>1 (REWRITE) (IMPLIES (AND (NOT (ILESSP A X)) (NOT (ILESSP 0 D)) (ILESSP 1 C)) (NOT (V&C-APPLY$ 'ITERK (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) '(1 . 0) (CONS X 0))))) ; hint ( (USE (ITERK-COST-IS-UNBOUNDED-WHEN-X<=A&D<=0&C>1 (I (ADD1 (CDR (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. (PROVE-LEMMA K-DOES-NOT-EXIST-WHEN-X<=A&D<=0&C>1 (REWRITE) (IMPLIES (AND (NOT (ILESSP A X)) (NOT (ILESSP 0 D)) (ILESSP 1 C)) (NOT (V&C-APPLY$ 'K (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS X 0))))) ; hint ( (expand (V&C-APPLY$ 'K (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS X 0)))) )) (PROVE-LEMMA K-DOES-NOT-HALT-WHEN-X<=A&D<=0&C>1 (REWRITE) (IMPLIES (AND VC-A VC-B VC-C VC-D VC-X (NOT (ILESSP (CAR VC-A)(CAR VC-X))) (NOT (ILESSP 0 (CAR VC-D))) (ILESSP 1 (CAR VC-C))) (NOT (V&C-APPLY$ 'K (LIST VC-A VC-B VC-C VC-D VC-X)))) ; hint ( (USE (EQ-ARGS-GIVE-EQ-EXISTENCE (FN 'K) (ARGS1 (LIST (CONS (CAR VC-A) 0) (CONS (CAR VC-B) 0) (CONS (CAR VC-C) 0) (CONS (CAR VC-D) 0) (CONS (CAR VC-X) 0))) (ARGS2 (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. (DEFN K-MEASURE ( A X ) (IF (ILESSP A X) 0 (IPLUS 1 (IPLUS A (INEG X))))) (PROVE-LEMMA K-MEASURE_X+D=X (REWRITE) (IMPLIES (AND (ILESSP 0 D) (NOT (ILESSP A X))) (LESSP (K-MEASURE A (IPLUS D X)) (K-MEASURE A X))) ; hint ( (DISABLE-THEORY INTEGERS NATURALS) (ENABLE-THEORY INTEGER-DEFNS) )) (DISABLE K-MEASURE) (DEFN INDUCT-HINT-K-MEASURE ( A B C D X ) (IF (NOT (ILESSP 0 D)) T (IF (ILESSP A X) T (INDUCT-HINT-K-MEASURE A B C D (IPLUS D X)))) ; hint ( (LESSP (K-MEASURE A X)) )) (PROVE-LEMMA ITERK-EXISTS-WHEN-D>0&C<=1&E=C (REWRITE) (IMPLIES (AND (ILESSP 0 D) (NOT (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)))) ; hint ( (INDUCT (INDUCT-HINT-K-MEASURE A B C D X)) )) (PROVE-LEMMA ITERK-EXISTS-WHEN-X<=A&D>0&C<=1&E=1 (REWRITE) (IMPLIES (AND (NOT (ILESSP A X)) (ILESSP 0 D) (NOT (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. (PROVE-LEMMA K-EXISTS-WHEN-X<=A&D>0&C<=1 (REWRITE) (IMPLIES (AND (NOT (ILESSP A X)) (ILESSP 0 D) (NOT (ILESSP 1 C))) (V&C-APPLY$ 'K (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS X 0)))) ; hint ( (expand (V&C-APPLY$ 'K (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS X 0)))) )) (PROVE-LEMMA K-HALTS-WHEN-X<=A&D>0&C<=1 (REWRITE) (IMPLIES (AND VC-A VC-B VC-C VC-D VC-X (NOT (ILESSP (CAR VC-A)(CAR VC-X))) (ILESSP 0 (CAR VC-D)) (NOT (ILESSP 1 (CAR VC-C)))) (V&C-APPLY$ 'K (LIST VC-A VC-B VC-C VC-D VC-X ))) ; hint ( (USE (EQ-ARGS-GIVE-EQ-EXISTENCE (FN 'K) (ARGS1 (LIST (CONS (CAR VC-A) 0) (CONS (CAR VC-B) 0) (CONS (CAR VC-C) 0) (CONS (CAR VC-D) 0) (CONS (CAR VC-X) 0))) (ARGS2 (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. (PROVE-LEMMA ITERK-EXISTS-WHEN-E<=1&A1-WHEN-X>0&X<>1 (REWRITE) (IMPLIES (AND (ILESSP 0 X) (NOT (EQUAL X 1))) (ILESSP 1 X)) ; hint ( (DISABLE-THEORY INTEGERS NATURALS) (ENABLE-THEORY INTEGER-DEFNS) )) (PROVE-LEMMA ITERK-EXISTS&ITERK>A-WHEN-X>A&B<=0&E>0 (REWRITE) (IMPLIES (AND (ILESSP A X) (NOT (ILESSP 0 B)) (ILESSP 0 E)) (AND (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))))))) ; hint ( (INDUCT (INDUCT-HINT-POSITIVE-INT E)) )) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; 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. (PROVE-LEMMA IPLUS_1_-1_X=X_WHEN_X>0 (REWRITE) (IMPLIES (ILESSP 0 X) (EQUAL (IPLUS 1 (IPLUS -1 X)) X)) ; hint ( (DISABLE-THEORY INTEGERS NATURALS) (ENABLE-THEORY INTEGER-DEFNS) )) (PROVE-LEMMA X+Y>1-WHEN-X>0&X<>1&0= 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. (PROVE-LEMMA N_C-1_+1=C-WHEN-N=1&C>1 (REWRITE) (IMPLIES (AND (EQUAL N 1) (ILESSP 1 C)) (EQUAL (IPLUS 1 (ITIMES N (IPLUS -1 C))) C)) ; hint ( (DISABLE-THEORY INTEGERS NATURALS) (ENABLE-THEORY INTEGER-DEFNS) )) (PROVE-LEMMA ND=D-WHEN-N=1&D>0 (REWRITE) (IMPLIES (AND (EQUAL N 1) (ILESSP 0 D)) (EQUAL (ITIMES N D) D)) ; hint ( (DISABLE-THEORY INTEGERS NATURALS) (ENABLE-THEORY INTEGER-DEFNS) )) (PROVE-LEMMA A>=X-WHEN-A+D>=X+D (REWRITE) (IMPLIES (NOT (ILESSP (IPLUS A D) (IPLUS X D))) (NOT (ILESSP A X)))) (PROVE-LEMMA ITERK_E=1+_N_C-1&X+ND-EXISTS-BASE-STEP (REWRITE) (IMPLIES (AND (EQUAL N 1) (ILESSP 1 C) (ILESSP 0 D) (NOT (ILESSP (IPLUS A D) (IPLUS X (ITIMES N D))))) (IFF (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))))) ; hint ( (DISABLE-THEORY INTEGERS) )) (PROVE-LEMMA ITERK_E=1+_N_C-1&X+ND-VALUE-BASE-STEP (REWRITE) (IMPLIES (AND (EQUAL N 1) (ILESSP 1 C) (ILESSP 0 D) (NOT (ILESSP (IPLUS A D) (IPLUS X (ITIMES N D))))) (EQUAL (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)))))) ; hint ( (DISABLE-THEORY INTEGERS) )) (PROVE-LEMMA N-1_C-1>0-WHEN-11 (REWRITE) (IMPLIES (AND (ILESSP 1 C) (ILESSP 0 N) (NOT (EQUAL N 1))) (ILESSP 0 (ITIMES (IPLUS -1 N) (IPLUS -1 C)))) ; hint ( (DISABLE-THEORY INTEGERS NATURALS) (ENABLE-THEORY INTEGER-DEFNS) )) (PROVE-LEMMA ITERK_E=1+_N_C-1&X+ND-EXISTS-STEP-1 (REWRITE) (IMPLIES (AND (ILESSP 1 C) (ILESSP 0 N) (NOT (EQUAL N 1))) (IFF (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))))))) ; hint ( (USE (NBR-OF-ITERATES-SUM-EXISTS&VALUES (E1 (ITIMES (IPLUS -1 N) (IPLUS -1 C))) (E2 1) (X (IPLUS X (ITIMES (IPLUS -1 N) D)))) (N-1_C-1>0-WHEN-11 (A A))) )) (PROVE-LEMMA ITERK_E=1+_N_C-1&X+ND-VALUE-STEP-1 (REWRITE) (IMPLIES (AND (ILESSP 1 C) (ILESSP 0 N) (NOT (EQUAL N 1))) (EQUAL (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)))))))) ; hint ( (USE (NBR-OF-ITERATES-SUM-EXISTS&VALUES (E1 (ITIMES (IPLUS -1 N) (IPLUS -1 C))) (E2 1) (X (IPLUS X (ITIMES (IPLUS -1 N) D)))) (N-1_C-1>0-WHEN-11 (A A))) (DISABLE NBR-OF-ITERATES-SUM-EXISTS&VALUES) )) (PROVE-LEMMA ITERK_E=1+_N_C-1&X+ND-EXISTS-STEP-2 (REWRITE) (IMPLIES (AND (ILESSP 0 N) (ILESSP 0 D) (NOT (ILESSP (IPLUS A D) (IPLUS X (ITIMES N D))))) (IFF (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))))))) ; hint ( (USE (EQ-ARGS-GIVE-EQ-EXISTENCE (FN 'ITERK) (ARGS1 (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))))) (ARGS2 (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))))))))) (PROVE-LEMMA ITERK_E=1+_N_C-1&X+ND-VALUE-STEP-2 (REWRITE) (IMPLIES (AND (ILESSP 0 N) (ILESSP 0 D) (NOT (ILESSP (IPLUS A D) (IPLUS X (ITIMES N D))))) (EQUAL (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)))))))) ; hint ( (USE (EQ-ARGS-GIVE-EQ-VALUES (FN 'ITERK) (ARGS1 (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))))) (ARGS2 (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))))))))) (PROVE-LEMMA ITERK_E=1+_N_C-1&X+ND-EXISTS-STEP-3 (REWRITE) (IMPLIES (AND (ILESSP 0 N) (NOT (EQUAL N 1)) (ILESSP 1 C)) (IFF (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))))) ; hint ( (USE (NBR-OF-ITERATES-SUM-EXISTS&VALUES (E1 (ITIMES (IPLUS -1 N) (IPLUS -1 C))) (E2 C) (X (IPLUS X (ITIMES N D)))) (N-1_C-1>0-WHEN-11 (A A))) (DISABLE ITERK-VALUE=BODY-VALUE-WHEN-E>1-VERSION-2 ITERK-VALUE=BODY-VALUE-WHEN-E>1-VERSION-3 NBR-OF-ITERATES-SUM-EXISTS&VALUES) )) (PROVE-LEMMA ITERK_E=1+_N_C-1&X+ND-VALUE-STEP-3 (REWRITE) (IMPLIES (AND (ILESSP 0 N) (NOT (EQUAL N 1)) (ILESSP 1 C)) (EQUAL (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)))))) ; hint ( (USE (NBR-OF-ITERATES-SUM-EXISTS&VALUES (E1 (ITIMES (IPLUS -1 N) (IPLUS -1 C))) (E2 C) (X (IPLUS X (ITIMES N D)))) (N-1_C-1>0-WHEN-11 (A A))) (DISABLE ITERK-VALUE=BODY-VALUE-WHEN-E>1-VERSION-2 ITERK-VALUE=BODY-VALUE-WHEN-E>1-VERSION-3 NBR-OF-ITERATES-SUM-EXISTS&VALUES) )) (PROVE-LEMMA A+D>=X+_N-1_D-WHEN-A+D>=X+ND&0=X+ND (REWRITE) (IMPLIES (AND (ILESSP 1 C) (ILESSP 0 D) (ILESSP 0 N) (NOT (ILESSP (IPLUS A D) (IPLUS X (ITIMES N D))))) (IFF (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))))) ; hint ( (INDUCT (INDUCT-HINT-POSITIVE-INT N)) (DISABLE-THEORY INTEGERS) )) (PROVE-LEMMA ITERK_E=1+_N_C-1&X+ND-VALUE-WHEN-1=X+ND (REWRITE) (IMPLIES (AND (ILESSP 1 C) (ILESSP 0 D) (ILESSP 0 N) (NOT (ILESSP (IPLUS A D) (IPLUS X (ITIMES N D))))) (EQUAL (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)))))) ; hint ( (INDUCT (INDUCT-HINT-POSITIVE-INT N)) (DISABLE-THEORY INTEGERS) )) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; 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. (DEFN N ( A D X ) (IF (NOT (ILESSP 0 D)) 0 (IF (ILESSP A X) 0 (IPLUS 1 (N A D (IPLUS X D))))) ; hint ( (LESSP (K-MEASURE A X)) )) (PROVE-LEMMA N>=0 (REWRITE) (NOT (ILESSP (N A D X) 0))) (PROVE-LEMMA N>0-WHEN-D>O&X<=A (REWRITE) (IMPLIES (AND (ILESSP 0 D) (NOT (ILESSP A X))) (ILESSP 0 (N A D X)))) (PROVE-LEMMA A=X+ND-WHEN-D>0&A>=X (REWRITE) (IMPLIES (AND (ILESSP 0 D) (NOT (ILESSP A X))) (NOT (ILESSP (IPLUS A D) (IPLUS X (ITIMES (N A D X) D)))))) (PROVE-LEMMA ITERK-E=1&X-IFF-ITERK_E=1+_N_C-1&X+ND-WHEN-1=X (REWRITE) (IMPLIES (AND (ILESSP 1 C) (ILESSP 0 D) (NOT (ILESSP A X))) (IFF (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))))) ; hint ( (DISABLE-THEORY INTEGERS) (USE (ITERK_E=1+_N_C-1&X+ND-EXISTS-WHEN-1=X+ND (N (N A D X)))) )) (PROVE-LEMMA ITERK-EXISTS-WHEN-E=1+N_C-1&X=X+ND&B<=0 (REWRITE) (IMPLIES (AND (NOT (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)))) ; hint ( (USE (ITERK-EXISTS&ITERK>A-WHEN-X>A&B<=0&E>0 (E (IPLUS 1 (ITIMES (N A D X) (IPLUS -1 C)))) (X (IPLUS X (ITIMES (N A D X) D)))) (A0&C<1&B<=0 (REWRITE) (IMPLIES (AND (NOT (ILESSP 0 B)) (ILESSP 1 C) (ILESSP 0 D) (NOT (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)))) ; hint ( (DISABLE-THEORY INTEGERS) )) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; 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. (PROVE-LEMMA K-EXISTS-WHEN-X<=A&D>0&C<1&B<=0 (REWRITE) (IMPLIES (AND (NOT (ILESSP 0 B)) (ILESSP 1 C) (ILESSP 0 D) (NOT (ILESSP A X))) (V&C-APPLY$ 'K (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS X 0)))) ; hint ( (DISABLE NBR-OF-ITERATES-SUM-EXISTS&VALUES ITERK_E=1+_N_C-1&X+ND-VALUE-BASE-STEP ITERK-VALUE=BODY-VALUE-WHEN-E>1-VERSION-3 ITERK-VALUE=BODY-VALUE-WHEN-E>1-VERSION-2) (EXPAND (V&C-APPLY$ 'K (LIST (CONS A 0) (CONS B 0) (CONS C 0) (CONS D 0) (CONS X 0)))) )) (PROVE-LEMMA K-HALTS-WHEN-X<=A&D>0&C<1&B<=0 (REWRITE) (IMPLIES (AND VC-A VC-B VC-C VC-D VC-X (NOT (ILESSP 0 (CAR VC-B))) (ILESSP 1 (CAR VC-C)) (ILESSP 0 (CAR VC-D)) (NOT (ILESSP (CAR VC-A) (CAR VC-X)))) (V&C-APPLY$ 'K (LIST VC-A VC-B VC-C VC-D VC-X))) ; hint ( (USE (EQ-ARGS-GIVE-EQ-EXISTENCE (FN 'K) (ARGS1 (LIST (CONS (CAR VC-A) 0) (CONS (CAR VC-B) 0) (CONS (CAR VC-C) 0) (CONS (CAR VC-D) 0) (CONS (CAR VC-X) 0))) (ARGS2 (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. (PROVE-LEMMA X+-X+Y=FIX-INT-Y (REWRITE) (IMPLIES (ILESSP 0 X) (EQUAL (IPLUS X (IPLUS (MINUS X) Y)) (FIX-INT Y))) ; hint ( (DISABLE-THEORY INTEGERS NATURALS) (ENABLE-THEORY INTEGER-DEFNS) )) (PROVE-LEMMA FIX-INT-X=X-WHEN-X>1 (REWRITE) (IMPLIES (ILESSP 1 X) (EQUAL (FIX-INT X) X)) ; hint ( (DISABLE-THEORY INTEGERS NATURALS) (ENABLE-THEORY INTEGER-DEFNS) )) (PROVE-LEMMA ITERK-E-X-IFF-ITERK-E-1-ITERK-1-X (REWRITE) (IMPLIES (ILESSP 1 E) (IFF (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))))))) ; hint ( (USE (NBR-OF-ITERATES-SUM-EXISTS&VALUES (E1 (IPLUS -1 E)) (E2 1))) (DISABLE NBR-OF-ITERATES-SUM-EXISTS&VALUES ITERK-VALUE=BODY-VALUE-WHEN-E>1-VERSION-3 ITERK-VALUE=BODY-VALUE-WHEN-E>1-VERSION-2 ITERK-EXISTS-IFF-BODY-EXISTS-WHEN-E>1-VERSION-3 ITERK-EXISTS-IFF-BODY-EXISTS-WHEN-E>1-VERSION-2) )) (PROVE-LEMMA ITERK-E-X=ITERK-E-1-ITERK-1-X (REWRITE) (IMPLIES (ILESSP 1 E)