anchor.diff:  	   (< (phi-2n-1 n phi0 v0 dv g1 dc) 0))
     :hints (("Goal"
   	   :use ((:instance phi-2n+1-<-0
  -			    (i n))))))
  -)
  +			    (n (1- n)))))))
  +)
  
positive.code:   				  (:python-file "phi-2n+1-smaller-than-0-base")
    				  (:let ())
    				  (:hypothesize ()))
  				state)))
    )
  
  (defthm phi-2n+1-<-0-base-new
      (implies (basic-params-equal (- i 2) 1 dc v0 dv g1 phi0)
  	   (< (phi-2n-1 (- i 1) phi0 v0 dv g1 dc) 0))
    :hints (("Goal''"
  	   :clause-processor
    	   (Smtlink clause
    				'( (:expand ((:function ())
    					     (:expansion-level 1)))
    				  (:python-file "phi-2n+1-smaller-than-0-base-new")
    				  (:let ())
    				  (:hypothesize ()))
  				state)))
    )
  
  (defthm phi-2n+1-<-0-base-corollary
    (implies (basic-params-equal (1- i) 2 dc v0 dv g1 phi0)
  	   (< (phi-2n-1 i phi0 v0 dv g1 dc) 0))
    :hints (("Goal"
  	   :use ((:instance phi-2n+1-<-0-base
  			    (n (- i 1))))))
    )
  
  (defthm phi-2n+1-<-0-base-corollary-2
    (implies (basic-params-equal (1- i) 2 dc v0 dv g1 phi0)
  	   (< (+ (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-base-corollary))))
    )
  
  (defthm stupid-proof
    (implies (and (equal a f)
  		(equal a i)
  		(implies (and m l) l)
  		(implies l (and c h))
  		(implies (and c h) (and c j))
  	        (implies (and a b c d) e)
  		(implies (and f b c d) g)
  		(implies (and f b h d e) g)
  		i
  		m
  		(implies (and a b j d) e)
  		f
  		b
  		l
  		d)
  	   g)
    :rule-classes nil)
  
  (defthm phi-2n+1-<-0-lemma-lemma1
    (implies
   (and
       (implies
            (and (and (integerp (+ -2 i))
                      (rationalp g1)
                      (rationalp v0)
                      (rationalp phi0)
                      (rationalp dv)
  		    (rationalp dc))
                 (equal (+ -2 i) 1)
                 (equal g1 1/3200)
  	       (>= dc 0)
  	       (< dc 1)
                 (<= 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))))))))
            (< (phi-2n-1 (+ -1 i) phi0 v0 dv g1 dc) 0))
       (implies
            (and (and (integerp (+ -1 i))
                      (rationalp g1)
                      (rationalp v0)
                      (rationalp phi0)
                      (rationalp dv)
  		    (rationalp dc))
                 (equal (+ -1 i) 2)
                 (equal g1 1/3200)
  	       (>= dc 0)
  	       (< dc 1)
                 (<= 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 i phi0 v0 dv g1 dc)
                  (* (/ (expt 5 (+ -2 i)))
                     (b-sum 1 (+ -2 i) v0 dv g1 dc)))
               0))
       (implies
            (and (and (integerp (+ -1 i))
                      (rationalp g1)
                      (rationalp v0)
                      (rationalp dv)
                      (rationalp phi0)
  		    (rationalp dc))
                 (<= 3 (+ -1 i))
                 (<= (+ -1 i) 640)
  	       (>= dc 0)
  	       (< 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)))))))
                 (< (phi-2n-1 (+ -1 i) phi0 v0 dv g1 dc) 0))
            (< (+ (a i phi0 v0 dv g1 dc)
                  (* (/ (expt 5 (+ -2 i)))
                     (b-sum 1 (+ -2 i) v0 dv g1 dc)))
               0))
       (not (or (not (integerp i)) (< i 1)))
       (implies
            (and (and (integerp (+ -1 -1 i))
                      (rationalp g1)
                      (rationalp v0)
                      (rationalp dv)
                      (rationalp phi0)
  		    (rationalp dc))
                 (<= 2 (+ -1 -1 i))
                 (<= (+ -1 -1 i) 640)
  	       (>= dc 0)
  	       (< 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 i) phi0 v0 dv g1 dc)
                  (* (/ (expt 5 (+ -2 -1 i)))
                     (b-sum 1 (+ -2 -1 i) v0 dv g1 dc)))
               0))
       (integerp (+ -1 i))
       (rationalp g1)
       (rationalp v0)
       (rationalp dv)
       (rationalp phi0)
       (rationalp dc)
       (<= 2 (+ -1 i))
       (<= (+ -1 i) 640)
       (>= dc 0)
       (< 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 i phi0 v0 dv g1 dc)
         (* (/ (expt 5 (+ -2 i)))
            (b-sum 1 (+ -2 i) v0 dv g1 dc)))
      0))
    :hints (("Goal"
  	   :use ((:instance stupid-proof
  			    (a (integerp (+ -1 -1 i)))
  			    (b (and (rationalp g1)
  				    (rationalp v0)
  				    (rationalp dv)
  				    (rationalp phi0)
  				    (rationalp dc)))
  			    (c (equal (+ -2 i) 1))
  			    (d (and (>= dc 0)
  				    (< 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)))))))))
  			    (e (< (+ (a (+ -1 i) phi0 v0 dv g1 dc)
  				     (* (/ (expt 5 (+ -2 -1 i)))
  					(b-sum 1 (+ -2 -1 i) v0 dv g1 dc)))
  				  0))
  			    (f (integerp (+ -1 i)))
  			    (g (< (+ (a i phi0 v0 dv g1 dc)
  				     (* (/ (expt 5 (+ -2 i)))
  					(b-sum 1 (+ -2 i) v0 dv g1 dc)))
  				  0))
  			    (h (and (<= 3 (+ -1 i))
  				    (<= (+ -1 i) 640)))
  			    (i (integerp i))
  			    (j (and (<= 2 (+ -1 -1 i))
  				    (<= (+ -1 -1 i) 640)))
  			    (l (and (<= 2 (+ -1 i))
  				    (<= (+ -1 i) 640)
  				    ))
  			    (m (>= i 1)))))))
  
  (defthm phi-2n+1-<-0-lemma-lemma2
    (implies (and (or (not (integerp i)) (< i 1))
                (integerp (+ -1 i))
                (rationalp g1)
                (rationalp v0)
                (rationalp dv)
                (rationalp phi0)
  	      (rationalp dc)
                (<= 2 (+ -1 i))
                (<= (+ -1 i) 640)
  	      (>= dc 0)
  	      (< 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 i phi0 v0 dv g1 dc)
                 (* (/ (expt 5 (+ -2 i)))
                    (b-sum 1 (+ -2 i) v0 dv g1 dc)))
              0))
    :rule-classes nil)
  
  (defthm phi-2n+1-<-0-lemma
    (implies (basic-params (1- i) 2 dc v0 dv g1 phi0)
  	   (< (+ (A i phi0 v0 dv g1 dc)
  		 (* (B-expt i)
  		    (B-sum 1 (- i 2) v0 dv g1 dc))) 0))
    :hints (("Goal"
  	   :do-not '(simplify)
  	   :induct (B-sum 1 i v0 dv g1 dc))
  	  ("Subgoal *1/2"
  	  :use ((:instance phi-2n+1-<-0-base-new)
  		(:instance phi-2n+1-<-0-base-corollary-2)
  		(:instance phi-2n+1-<-0-inductive-corollary-2)
  		))
  	  ("Subgoal *1/2''"
  	   :use ((:instance phi-2n+1-<-0-lemma-lemma1)))
  	  ("Subgoal *1/1'"
  	   :use ((:instance phi-2n+1-<-0-lemma-lemma2)))
  	  )
    )
  
  (defthm phi-2n+1-<-0
    (implies (basic-params (1- i) 2 dc v0 dv g1 phi0)
  	   (< (phi-2n-1 i phi0 v0 dv g1 dc) 0))
    :hints (("Goal"
  	   :use ((:instance phi-2n+1-<-0-lemma))
  	   ))
    )
  
  (defthm phi-2n-1-<-0
  
negative.code: 		 (:instance except-for-delta-<-0)))))
  
  (defthm phi-2n+1-<-0-inductive-corollary
    (implies (basic-params n 3 dc v0 dv g1 phi0
                           (< (+ (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))
    :hints (("Goal"
             :use ((:instance phi-2n+1-<-0-inductive)))))
  
  (defthm phi-2n+1-<-0-base-lemma
    (IMPLIES (AND (RATIONALP DC)
                  (RATIONALP V0)
                  (RATIONALP PHI0)
                  (RATIONALP DV)
                  (<= 0 DC)
                  (< DC 1)
                  (<= 1 (* 10/9 V0))
                  (<= V0 11/10)
                  (<= (- (* 8000 DV)) 1)
                  (<= (* 8000 DV) 1)
                  (<= 0 PHI0)
                  (< PHI0
                     (+ -1
                        (* (+ 1 DV V0)
                           (/ (+ 2561/3200 V0 (* 1/3200 DC)))))))
             (< (+ (* 1/3125 PHI0)
                   (* (+ 1 DV V0)
                      (/ (+ 3201/3200 V0 (* 1/3200 DC))))
                   (* 1/125 (+ 1 DV V0)
                      (/ (+ 1599/1600 V0 (* 1/3200 DC))))
                   (* 1/25 (+ 1 DV V0)
                      (/ (+ 3199/3200 V0 (* 1/3200 DC))))
                   (* 1/625 (+ 1 DV V0)
                      (/ (+ 3197/3200 V0 (* 1/3200 DC)))))
                656/625))
    :hints (("Goal"
  	   :clause-processor
    	   (Smtlink clause
    				'( (:expand ((:function ())
  