anchor.diff:  
   ;; for induction step 
   (encapsulate ()
  -	     
  +
   (defthm phi-2n+1-<-0-inductive
     (implies (basic-params n 3 dc v0 dv g1 phi0 (< (phi-2n-1 n phi0 v0 dv g1 dc) 0))
   	   (< (phi-2n-1 (1+ n) phi0 v0 dv g1 dc) 0))
  
positive.code: 		 (:instance except-for-delta-<-0)))))
  
  (defthm phi-2n+1-<-0-inductive-corollary
    (implies (basic-params (- i 1) 3 dc v0 dv g1 phi0
  			 (< (phi-2n-1 (- i 1) phi0 v0 dv g1 dc) 0))
  	   (< (phi-2n-1 i phi0 v0 dv g1 dc) 0))
    :hints (("Goal"
  	   :use ((:instance phi-2n+1-<-0-inductive
  			    (n (- i 1)))))))
  
  (defthm phi-2n+1-<-0-inductive-corollary-2
    (implies (basic-params (- i 1) 3 dc v0 dv g1 phi0
  			 (< (phi-2n-1 (- i 1) phi0 v0 dv g1 dc) 0))
  	   (< (+ (A i phi0 v0 dv g1 dc)
  		 (* (B-expt i)
  		    (B-sum 1 (- i 2) v0 dv g1 dc))) 0))
    :hints (("Goal"
  	   :use ((:instance phi-2n+1-<-0-inductive-corollary)))))
  
  (defthm phi-2n+1-<-0-base
      (implies (basic-params-equal n 2 dc v0 dv g1 phi0)
  	   (< (phi-2n-1 (1+ n) phi0 v0 dv g1 dc) 0))
    :hints (("Goal''"
  	   :clause-processor
    	   (Smtlink clause
    				'( (:expand ((:function ())
  
negative.code:   				  (:python-file "phi-2n+1-smaller-than-0-base")
    				  (:let ())
    				  (:hypothesize ()))
            state)))
    )
  
  (defthm phi-2n+1-<-0-base
      (implies (basic-params-equal n 2 dc v0 dv g1 phi0)
  	   (< (phi-2n-1 (1+ n) phi0 v0 dv g1 dc) 0))
    :hints (("Goal"
             :use ((:instance phi-2n+1-<-0-base-lemma))))
    )
  
  (defthm phi-2n+1-<-0-lemma-stupid-lemma1
    (IMPLIES
   (AND
       (EQUAL N 2)
       (NOT (OR (NOT (INTEGERP N)) (< N 1)))
       (IMPLIES
            (AND (AND (INTEGERP (+ -1 N))
                      (RATIONALP DC)
                      (RATIONALP G1)
                      (RATIONALP V0)
                      (RATIONALP DV)
                      (RATIONALP PHI0))
                 (<= 2 (+ -1 N))
                 (<= (+ -1 N) 640)
                 (<= 0 DC)
                 (< DC 1)
                 (EQUAL G1 1/3200)
                 (<= 9/10 V0)
                 (<= V0 11/10)
                 (<= -1/8000 DV)
                 (<= DV 1/8000)
                 (<= 0 PHI0)
                 (< PHI0
                    (+ -1
                       (* (FIX (+ 1 (FIX (+ V0 DV))))
                          (/ (+ 1
                                (FIX (* (+ 1
                                           (* (+ (FIX (* (+ 1 (FIX V0)) 1)) -1)
                                              (/ G1))
                                           -640 DC)
                                        G1))))))))
            (< (+ (A (FIX N) PHI0 V0 DV G1 DC)
                  (* (B-EXPT (FIX N))
                     (B-SUM 1 (+ -1 -1 N) V0 DV G1 DC)))
               0))
       (INTEGERP N)
       (RATIONALP DC)
       (RATIONALP G1)
       (RATIONALP V0)
       (RATIONALP DV)
       (RATIONALP PHI0)
       (<= 2 N)
       (<= N 640)
       (<= 0 DC)
       (< DC 1)
       (EQUAL G1 1/3200)
       (<= 9/10 V0)
       (<= V0 11/10)
       (<= -1/8000 DV)
       (<= DV 1/8000)
       (<= 0 PHI0)
       (< PHI0
          (+ -1
             (* (FIX (+ 1 (FIX (+ V0 DV))))
                (/ (+ 1
                      (FIX (* (+ 1
                                 (* (+ (FIX (* (+ 1 (FIX V0)) 1)) -1)
                                    (/ G1))
                                 -640 DC)
                              G1))))))))
   (< (+ (A (+ 1 N) PHI0 V0 DV G1 DC)
         (* (B-EXPT (+ 1 N))
            (B-SUM 1 (+ -1 N) V0 DV G1 DC)))
      0)))
  
  (defthm phi-2n+1-<-0-lemma-stupid-lemma2
    (IMPLIES
   (AND
       (IMPLIES
            (AND (AND (INTEGERP N)
                      (RATIONALP DC)
                      (RATIONALP G1)
                      (RATIONALP V0)
                      (RATIONALP DV)
                      (RATIONALP PHI0))
                 (<= 3 N)
                 (<= N 640)
                 (<= 0 DC)
                 (< DC 1)
                 (EQUAL G1 1/3200)
                 (<= 9/10 V0)
                 (<= V0 11/10)
                 (<= -1/8000 DV)
                 (<= DV 1/8000)
                 (<= 0 PHI0)
                 (< PHI0
                    (+ -1
                       (* (FIX (+ 1 (FIX (+ V0 DV))))
                          (/ (+ 1
                                (FIX (* (+ 1
                                           (* (+ (FIX (* (+ 1 (FIX V0)) 1)) -1)
                                              (/ G1))
                                           -640 DC)
                                        G1)))))))
                 (< (+ (A N PHI0 V0 DV G1 DC)
                       (* (B-EXPT N)
                          (B-SUM 1 (+ -1 -1 N) V0 DV G1 DC)))
                    0))
            (< (+ (A (+ 1 N) PHI0 V0 DV G1 DC)
                  (* (B-EXPT (+ 1 N))
                     (B-SUM 1 (+ -1 N) V0 DV G1 DC)))
               0))
       (< 2 N)
       (NOT (OR (NOT (INTEGERP N)) (< N 1)))
       (IMPLIES
            (AND (AND (INTEGERP (+ -1 N))
                      (RATIONALP DC)
                      (RATIONALP G1)
                      (RATIONALP V0)
                      (RATIONALP DV)
                      (RATIONALP PHI0))
                 (<= 2 (+ -1 N))
                 (<= (+ -1 N) 640)
                 (<= 0 DC)
                 (< DC 1)
                 (EQUAL G1 1/3200)
                 (<= 9/10 V0)
                 (<= V0 11/10)
                 (<= -1/8000 DV)
                 (<= DV 1/8000)
                 (<= 0 PHI0)
                 (< PHI0
                    (+ -1
                       (* (FIX (+ 1 (FIX (+ V0 DV))))
                          (/ (+ 1
                                (FIX (* (+ 1
                                           (* (+ (FIX (* (+ 1 (FIX V0)) 1)) -1)
                                              (/ G1))
                                           -640 DC)
                                        G1))))))))
            (< (+ (A (FIX N) PHI0 V0 DV G1 DC)
                  (* (B-EXPT (FIX N))
                     (B-SUM 1 (+ -1 -1 N) V0 DV G1 DC)))
               0))
       (INTEGERP N)
       (RATIONALP DC)
       (RATIONALP G1)
       (RATIONALP V0)
       (RATIONALP DV)
       (RATIONALP PHI0)
       (<= 2 N)
       (<= N 640)
       (<= 0 DC)
       (< DC 1)
       (EQUAL G1 1/3200)
       (<= 9/10 V0)
       (<= V0 11/10)
       (<= -1/8000 DV)
       (<= DV 1/8000)
       (<= 0 PHI0)
       (< PHI0
          (+ -1
             (* (FIX (+ 1 (FIX (+ V0 DV))))
                (/ (+ 1
                      (FIX (* (+ 1
                                 (* (+ (FIX (* (+ 1 (FIX V0)) 1)) -1)
                                    (/ G1))
                                 -640 DC)
                              G1))))))))
   (< (+ (A (+ 1 N) PHI0 V0 DV G1 DC)
         (* (B-EXPT (+ 1 N))
            (B-SUM 1 (+ -1 N) V0 DV G1 DC)))
      0)))
  
  (defthm phi-2n+1-<-0-lemma
    (IMPLIES (basic-params n 2 dc v0 dv g1 phi0)
             (< (+ (A (+ 1 n) phi0 V0 DV g1 dc)
                   (* (B-EXPT (+ 1 N))
                      (B-SUM 1 (+ -1 N) V0 DV g1 dc)))
                0))
    :hints (("Goal"
             :do-not '(simplify)
             :in-theory (disable B-expt)
             :induct (B-sum 1 N V0 DV g1 dc)
             )
            ("Subgoal *1/2"
             :cases ((< n 2) (equal n 2) (> n 2)))
            ("Subgoal *1/2.2"
             :use ((:instance phi-2n+1-<-0-base)
                   (:instance phi-2n+1-<-0-lemma-stupid-lemma1)))
            ("Subgoal *1/2.1"
             :use ((:instance phi-2n+1-<-0-inductive-corollary)
                   (:instance phi-2n+1-<-0-lemma-stupid-lemma2)))
            ))
  
  (defthm phi-2n+1-<-0
    (implies (basic-params n 2 dc v0 dv g1 phi0)
  	   (< (phi-2n-1 (1+ n) phi0 v0 dv g1 dc) 0))
    :hints (("Goal"
             :use ((:instance phi-2n+1-<-0-lemma))))
    )
  
  (defthm phi-2n-1-<-0
  